\newif\ifnotes
\notestrue

\documentclass[a4paper,11pt]{article}
\usepackage{breakcites}
\usepackage{fullpage}
\usepackage{amsmath, amsthm, times, amssymb}
\usepackage[table]{xcolor}
\usepackage[hypertexnames=false]{hyperref}
\usepackage{xspace}
\renewcommand{\paragraph}[1]{\vspace{1.5mm}\noindent \textbf{#1}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%general\
%\renewcommand{\vec}[1]{\mathbf{#1}}
\renewcommand{\cal}{\mathcal}
\newcommand{\bb}{\mathbb}
\newcommand{\ve}[1]{\langle #1 \rangle}
\newcommand{\samp}[1]{\overset{#1}{\leftarrow}}
\newcommand{\set}[1]{\left\{#1\right\}}
\newcommand{\abs}[1]{\left|#1\right|}
\newcommand{\labs}{\left |}
\newcommand{\rabs}{\right |}
\renewcommand{\)}{\right )}
\renewcommand{\]}{\right ]}
\renewcommand{\(}{\left (}
\renewcommand{\[}{\left [}
\newcommand{\pST}{\; \middle\vert \;}
\newcommand{\zo}{\{0,1\}}
\newcommand{\Nat}{\mathbb{N}}
\newcommand{\E}{\mathcal{E}}
\newcommand{\poly}{\mathrm{poly}}
\newcommand{\negl}{\mathrm{negl}}
\newcommand{\superpoly}{\mathrm{superpoly}}
\newcommand{\polylog}{\mathrm{polylog}}
\newcommand{\pprime}{p}
\newcommand{\zp}{\mathbb{Z}_\pprime}
\newcommand{\prot}[2]{\ve{#1,#2}}

%LDE
\newcommand{\Iden}{\beta}

% Languages and Relations
\newcommand{\lang}{\mathcal{L}}
\newcommand{\rell}{\mathcal{R}_\mathcal{L}}
\newcommand{\ins}{x}
\newcommand{\wit}{w}
\newcommand{\Time}{T}

%general algo
\newcommand{\secp}{n}
\newcommand{\Adv}{\mathsf{Adv}}
\newcommand{\Poly}{p}

%graded encoding
\newcommand{\pp}{{\sf pp}}
\newcommand{\InstGen}{\mathsf{InstGen}}
\newcommand{\Samp}{\mathsf{Samp}}
\newcommand{\Enc}{\mathsf{Encode}}
\newcommand{\Add}{\mathsf{Add}}
\newcommand{\Sub}{\mathsf{Sub}}
\newcommand{\Mult}{\mathsf{Mult}}
\newcommand{\isZero}{\mathsf{isZero}}
\newcommand{\level}{k}
\newcommand{\edegree}{\delta}
\newcommand{\Senc}[2]{E^{#1}_{#2}}
\newcommand{\enc}[2]{\[{#1}\]_{#2}}
\newcommand{\uenc}{u}
\newcommand{\relm}{r}
\newcommand{\telm}{t}
\newcommand{\zerolevel}{{ \vec{\bf 0}}}
\newcommand{\vlevel}{{\bf v}}
\newcommand{\ulevel}{{\bf u}}
\newcommand{\elevel}{{\bf e}}
\newcommand{\slevel}{{\bf s}}

%SNARKs
\newcommand{\Gen}{\mathsf{Gen}}
\renewcommand{\P}{\mathsf{P}}
\newcommand{\V}{\mathsf{V}}
\newcommand{\cPins}{\mathsf{{P^*_1}}}
\newcommand{\cPproof}{\mathsf{{P^*_2}}}
\newcommand{\CRS}{\mathsf{CRS}}
\newcommand{\Proof}{\Pi}
\newcommand{\cProof}{\Pi^*}
\newcommand{\Psize}{Q_{\P}}
\newcommand{\Vsize}{Q_{\V}}

% sum check
\newcommand{\scGen}{\Gen_{SC}}
\newcommand{\scP}{\P_{SC}}
\newcommand{\scV}{\V_{SC}}
\newcommand{\cscP}{\mathsf{{P^*_{SC}}}}

\newcommand{\func}{f}
\newcommand{\gfunc}{g}
\newcommand{\mvars}{m}
\newcommand{\mvarsy}{{m_1}}
\newcommand{\mvarsz}{{m_2}}
\newcommand{\llen}{l}
\newcommand{\lleny}{{l_1}}
\newcommand{\llenz}{{l_2}}
\newcommand{\xinp}{x}
\newcommand{\yinp}{y}
\newcommand{\zinp}{z}
\newcommand{\vxinp}{{\bf x}}
\newcommand{\vyinp}{{\bf y}}
\newcommand{\vzinp}{{\bf z}}

\newcommand{\winp}{w}
\newcommand{\winpo}{w^{\sf out}}
\newcommand{\winpc}{w^*}
\newcommand{\vwinp}{{\bf w}}
\newcommand{\vwinpo}{{\bf w^{\sf out}}}
\newcommand{\vwinpc}{{\bf w^*}}

\newcommand{\vval}{c}
\newcommand{\vvalo}{c^{\sf out}}
\newcommand{\vvalc}{c^*}
\newcommand{\vvala}{c^+}
\newcommand{\vvals}{c^-}
\newcommand{\vvalm}{c^\times}

\newcommand{\inso}{y}
\newcommand{\insc}{y^*}
\newcommand{\Echeat}{{\sf CHEAT}}
\newcommand{\ES}{{\sf S}}

% 2-to-1
\newcommand{\ttoGen}{\Gen_{2\rightarrow 1}}
\newcommand{\ttoP}{\P_{2\rightarrow 1}}
\newcommand{\ttoV}{\V_{2\rightarrow 1}}
\newcommand{\zline}{\vec \gamma}



% BB protocol
\newcommand{\bbGen}{\Gen_{BB}}
\newcommand{\bbP}{\P_{BB}}
\newcommand{\bbV}{\V_{BB}}
\newcommand{\Cir}{C}
\newcommand{\inpS}{k}
\newcommand{\cirS}{S}
\newcommand{\cirD}{d}
\newcommand{\gate}{g}
\newcommand{\Fadd}{\mathsf{add}}
\newcommand{\Fsub}{\mathsf{sub}}
\newcommand{\Fmult}{\mathsf{mult}}
\newcommand{\EFadd}{\widetilde{\mathsf{add}}}
\newcommand{\EFsub}{\widetilde{\mathsf{sub}}}
\newcommand{\EFmult}{\widetilde{\mathsf{mult}}}
\newcommand{\Fcir}{\mathsf{V}}
\newcommand{\EFcir}{\widetilde{\mathsf{V}}}

\newcommand{\scProof}{\Proof_{SC}}
\newcommand{\ttoProof}{\Proof_{2\rightarrow 1}}
\newcommand{\cscProof}{{\Proof^*}^{SC}}
\newcommand{\cttoProof}{{\Proof^*}^{2\rightarrow 1}}
\newcommand{\scCRS}{\mathsf{CRS}_{SC}}
\newcommand{\ttoCRS}{\mathsf{CRS}_{2\rightarrow 1}}
\newcommand{\scins}{\ins_{SC}}
\newcommand{\ttoins}{\ins_{2\rightarrow 1}}
\newcommand{\scinso}{\inso_{SC}}
\newcommand{\ttoinso}{\inso_{2\rightarrow 1}}
\newcommand{\scEcheat}{{\sf CHEAT}_{SC}}
\newcommand{\ttoEcheat}{{\sf CHEAT}_{2\rightarrow 1}}
\newcommand{\Eout}{{\sf OUT}}

% Textual abbreviations (not for mathematical expressions)
\newcommand{\textabbrevstyle}[1]{\mbox{#1}}
\newcommand{\textabbrevstylebol}[1]{\mbox{\bf #1}}
\newcommand{\newtextabbrev}[1]{\expandafter\newcommand\csname #1\endcsname{\textabbrevstyle{#1}\xspace}}
\newcommand{\renewtextabbrev}[1]{\expandafter\renewcommand\csname #1\endcsname{\textabbrevstyle{#1}\xspace}}

\newcommand{\newtextabbrevbol}[1]{\expandafter\newcommand\csname #1\endcsname{\textabbrevstylebol{#1}\xspace}}
\newcommand{\renewtextabbrevbol}[1]{\expandafter\renewcommand\csname
#1\endcsname{\textabbrevstylebol{#1}\xspace}}

\newtextabbrev{OWF}
\newtextabbrev{pvSNARG}
\newtextabbrev{PPT}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newtheorem{definition}{Definition}[section]
\newtheorem{lemma}{Lemma}[section]
\newtheorem{corollary}{Corollary}[section]
\newtheorem{theorem}{Theorem}[section]
\newtheorem{claim}{Claim}[section]
\newtheorem{assumption}{Assumption}[section]
\newtheorem{proposition}{Proposition}[section]
\newtheorem{hypothesis}{Hypothesis}[section]
\newtheorem{observation}{Observation}[section]
\theoremstyle{remark}
\newtheorem{construction}{Construction}[section]
\newtheorem{remark}{Remark}[section]
\newtheorem{example}{Example}[section]
\newtheorem{fact}{Fact}[section]
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\secref}[1]{Section~\protect\ref{#1}}
\newcommand{\appref}[1]{Appendix~\protect\ref{#1}}
\newcommand{\defref}[1]{Definition~\protect\ref{#1}}
\newcommand{\assref}[1]{Assumption~\protect\ref{#1}}
\newcommand{\conref}[1]{Construction~\protect\ref{#1}}
\newcommand{\figref}[1]{Figure~\protect\ref{#1}}
\newcommand{\tblref}[1]{Table~\protect\ref{#1}}
\newcommand{\thmref}[1]{Theorem~\protect\ref{#1}}
\newcommand{\prpref}[1]{Proposition~\protect\ref{#1}}
\newcommand{\lemref}[1]{Lemma~\protect\ref{#1}}
\newcommand{\clmref}[1]{Claim~\protect\ref{#1}}
\newcommand{\corref}[1]{Corollary~\protect\ref{#1}}
\newcommand{\fctref}[1]{Fact~\protect\ref{#1}}
\newcommand{\eqnref}[1]{Equation~\protect\ref{#1}}
\newcommand{\algref}[1]{Algorithm~(\protect\ref{#1})}
\newcommand{\remref}[1]{Remark~\protect\ref{#1}}
\newcommand{\proref}[1]{Protocol~\protect\ref{#1}}
\newcommand{\stpref}[1]{Step~\protect\ref{#1}}
\newcommand{\tstref}[1]{Test~\protect\ref{#1}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newenvironment{boxfig}[2]{\begin{figure}[#1]\fbox{\begin{minipage}{\linewidth}
                        %\vspace{0.2em}
                        \makebox[0.025\linewidth]{}
                        \begin{minipage}{0.95\linewidth}
            {\small{
                        #2 }}
                        \end{minipage}
                        %\vspace{0.2em}
                        \end{minipage}}}{\end{figure}}


\newcommand{\pprotocol}[4]{
\begin{boxfig}{h!}{
\begin{center}
{\bf #1}
\end{center}
    #4
\vspace{0.5ex} } \caption{\label{#3} #2}
\end{boxfig}
}

\newcommand{\protocol}[4]{
\pprotocol{#1}{#2}{#3}{#4} }
%Example:
%\protocol{Header}{Caption}{label}{the protocol}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\ifnotes
\newcommand{\omer}[1]{$\ll$\textsf{\color{red} Omer: { #1}}$\gg$}
\newcommand{\guy}[1]{$\ll$\textsf{\color{orange} Guy: { #1}}$\gg$}
\else
\newcommand{\omer}[1]{}
\newcommand{\guy}[1]{}
\fi



\begin{document}
\author{
Omer Paneth\thanks{Boston University. Email: \texttt{omer@bu.edu}.  Supported by the Simons award for graduate students in theoretical computer science and an NSF Algorithmic foundations grant 1218461.}
\and
Guy N. Rothblum\thanks{\guy{Affiliation?}. Email: \texttt{rothblum@alum.mit.edu}.}
}


\title{Publicly-Verifiable Delegation from Graded Encodings}
\maketitle

\begin{abstract}
\end{abstract}

\thispagestyle{empty}
\newpage
\pagenumbering{arabic}
\section{Introduction}

\section{Tools and Definitions}

\subsection{Graded Encodings}\label{sec:graded_enc}

Graded (multi-linear) encoding schemes were introduced by Garg, Gentry and Halevi \cite{GargGH13}. \guy{For delegation for P we can use symmetric maps}

We rely on ``asymmetric'' graded encoding, where an encodings {\em level} is a vector in $\Nat^\level$. We define a partial order over levels.

\begin{definition}[Partial order over $\Nat^\level$]
For $\level \in \Nat$ and tow vectors $\vlevel,\ulevel \in \Nat^\level$ we define:
$$\vlevel \leq \ulevel \quad \Leftrightarrow \quad \forall i \in [\level]: \vlevel[i] \leq \ulevel[i]\enspace.$$

In whet follows we use the following notation: for $\edegree \in \Nat$ and $\vlevel,\ulevel  \in \Nat^\level$ let $\vlevel+\ulevel$ be the point-wise addition of $\vlevel$ and $\ulevel$, and let $\edegree\cdot \vlevel$ be the vector $\vlevel$ where every coordinate is multiplied by $\edegree$. Let $\Lambda(\level,\edegree)$ be the set:
$$\set{\vlevel \in \Nat^\level : \forall i \in [\level], \vlevel[i] \leq \edegree}\enspace.$$
For $i \in [\level]$ let $\elevel_i(\level)$ be the vector in $\Nat^\level$ that is $0$ everywhere except for the $i$-th coordinate, where it is $1$, and let $\slevel_{i}(\level)$ be the all 1's vector: $$\slevel_{i}(\level) = \sum_{j \in [i]}[\elevel_i(\level)] \enspace.$$
When $\level$ is clear from the context we simply write $\elevel_{i}$ and $\slevel_{i}$.
\end{definition}

\begin{definition} [Graded Encoded Scheme] A graded encoding scheme is associated with a tuple of
PPT algorithms $(\InstGen, \Samp, \Enc, \Add, \Sub, \Mult, \isZero)$ as follows:
\begin{itemize}
\item {\bf Instance Generation:} $\InstGen$ takes as input the security parameter $1^n$ and multi-linearity parameters
$\level,\edegree$, and outputs public parameters $\pp$, which define an underlying ring~$R$. We restrict our attention to graded encoding schemes where $R$ is $\zp$ and $p$ is a prime of size exponential in $n$.
The public parameters $\pp$ determine a collection of sets $\set{\Senc{\alpha}{\vlevel}: \vlevel \in \Lambda(\level,\edegree), \alpha \in R}$.
\item {\bf Sampling:} $\Samp$ takes as input the public parameters $\pp$, and outputs a level-zero encoding in $\Senc{\alpha}{\zerolevel}$ where $\alpha$ is a uniformly distributed element in $R$.
\item {\bf Encoding:} $\Enc$ takes as input the public parameters $\pp$, a level-zero encoding $\uenc \in \Senc{\alpha}{\zerolevel}$ and an index of a level $\vlevel \in \Lambda(\level,\edegree)$ and outputs an encoding in $\Senc{\alpha}{\vlevel}$.
\item {\bf Addition:} $\Add$ takes as input the public parameters $\pp$ and two encodings $\uenc_1\in \Senc{\alpha_1}{\vlevel}$ and $\uenc_2\in \Senc{\alpha_2}{\vlevel}$ such that $\uenc_1, \uenc_2$ are in the same level $\vlevel$, and outputs an encoding in $\Senc{\alpha_1+\alpha_2}{\vlevel}$.
\item {\bf Subtraction:} $\Sub$ takes as input the public parameters $\pp$ and two encodings $\uenc_1\in \Senc{\alpha_1}{\vlevel}$ and $\uenc_2\in \Senc{\alpha_2}{\vlevel}$ such that $\uenc_1, \uenc_2$ are in the same level $\vlevel$, and outputs an encoding in $\Senc{\alpha_1-\alpha_2}{\vlevel}$.
\item {\bf Multiplication:} $\Mult$ takes as input the public parameters $\pp$ and encodings $\uenc_1\in \Senc{\alpha_1}{\vlevel_1}$ and  $\uenc_2\in \Senc{\alpha_2}{\vlevel_2}$ such that $\vlevel_1 + \vlevel_2 \in \Lambda(\level,\edegree)$, and outputs an encoding in $\Senc{\alpha_1\cdot\alpha_2}{\vlevel_1 + \vlevel_2}$.
 \item {\bf Zero testing:} $\isZero$ takes as input the public parameters $\pp$ and an encoding in $\Senc{\alpha}{\vlevel}$ for $\vlevel \in \Lambda(\level,\edegree)$ and outputs 1 if and only if $\alpha = 0$.
\end{itemize}
We also assume that the public parameters $\pp$ include a single encoding in $\Senc{0}{\zerolevel}$ and a single encoding in $\Senc{1}{\zerolevel}$. We often denote an element in $\Senc{\alpha}{\vlevel}$ by $\enc{\alpha}{\vlevel}$. \guy{We should mention that there is error, but we ignore it. Also means we don't have perfect completeness.}
\end{definition}

We formulate the following hardness assumption on graded encoding schemes. Roughly speaking, we assume that given an encoding of a random element $\alpha \in R$ in some level $\elevel_i$ is it hard to find encodings of $\beta,\gamma \in R$ in a level ``smaller than $j \cdot \elevel_i$'', such that $\beta \cdot \alpha^j = \gamma$.
\begin{assumption}\label{ass.assumption1}[\guy{Name the assumption?}]
Let $\level = \level(n),\edegree = \edegree(n)$ be polynomials.
For every poly-size adversary $\Adv$ there exists a negligible function $\mu$ such that for every $n \in \Nat$ and for every $i \in [\level], j \in [\edegree]$:
$$\Pr\[
\begin{array}{l}
\pp \gets \InstGen(1^n,\level(n),\edegree(n));\\
\enc{\alpha}{\zerolevel} \gets \Samp(\pp);\\
\enc{\alpha}{\elevel_i} \gets \Enc(\pp,\enc{\alpha}{\zerolevel},\elevel_i);\\
\enc{\beta}{\vlevel},\enc{\gamma}{\vlevel} \gets \Adv(\pp,\enc{\alpha}{\elevel_i}); \\
\(\beta \cdot \alpha^j = \gamma\) \quad \land \quad \(\beta \neq 0\) \quad \land \quad  \(j \cdot \elevel_i \not\leq \vlevel\)
\end{array}
\] \leq \mu(n)\enspace,$$
where the arithmetics is over the ring $R$ defined by $\pp$.
\end{assumption}

\guy{change numbering so the assumption/remarks are not overloaded}

\begin{remark}\label{remark.falsifiable1}
Assumption \ref{ass.assumption1} is {\em falsifiable} \cite{Naor}. We can efficiently check whether the encodings returned by $\Adv$ satisfy the equation $\beta \cdot \alpha^j = \gamma$ (and $\beta \neq 0$). This condition can be verified using the public parameters $\pp$ and the operations $\Add, \Sub, \Mult, \isZero$, applied to the adversary's output encodings. Note that in particular, this does not require finding the encoded ring elements $\beta, \gamma$ and without knowing the description of the ring $R$. For simplicity of notations we do not explicitly describe this efficient verification procedure as part of \assref{ass.assumption1}.
\end{remark}

\subsection{(Publicly-Verifiable) Non-Interactive Arguments}

We define (publicly verifiable) non-interactive arguments and some properties of interest. \guy{Let's find a word to replace succinct, which implies NP languages. We can call it an ``efficient'' argument system. Or find a better / less ambiguous word}

\begin{definition}[Non-Interactive Argument]
A tuple of \PPT algorithms $(\Gen,\P,\V)$ are a (publicly verifiable) non-interactive argument for a language $\lang$ if they are as follows. Let $m = m(n)$ be a polynomial. For security parameter $n \in \Nat$, and for instance $\ins \in \zo^{m}$,  $\Gen(1^n)$ outputs a string $\CRS$, $\P(\CRS,\ins)$ outputs a proof $\Proof$ and $\V(\CRS,\ins,\Proof)$ outputs one bit indicating acceptance or rejection. We require completeness and soundness:

\begin{itemize}
  \item \underline{Completeness.} There exists a negligible function $\mu$ such that for every $n \in \Nat$, and for every $\ins \in \lang \cap \zo^{m}$:
      $$\Pr\[
        \begin{array}{l}
        \CRS \gets \Gen(1^n); \\
        \Proof \gets \P(\CRS,\ins); \\
        \V(\CRS , \ins \Proof) = 1
        \end{array}
        \] \geq 1 - \mu(n) \enspace.$$
  \item \underline{Adaptive Soundness.}
  for every pair of poly-size circuits $\cPins, \cPproof$ there exists a negligible function $\mu$ such that for every $n \in \Nat$:
      $$\Pr\[
        \begin{array}{l}
        \CRS \gets \Gen(1^n); \\
        \ins^* \gets \cPins(\CRS);\\
        \cProof \gets \cPproof(\CRS,\ins^*); \\
        \V(\CRS , \ins^* ,\cProof) = 1 \quad \land \quad \ins^* \notin \lang
        \end{array}
        \] \leq \mu(n)\enspace.$$
\end{itemize}

We say that an argument system is {\em efficient} if the running time of $\P$ is at most $\Psize(n, m)$ and the running time of $\V$ is at most $\Vsize(n, \log(m)).$ \guy{need better word than efficient. Also define depth-efficient (and space-efficient?)}

\end{definition}

\subsection{Ring-Independent Arithmetic Circuits.}
In this section we define ring-independent arithmetic circuits. These are arithmetic circuits that evaluate to the same values on the boolean hypercube over any ring. We choose to work with  ring-independent arithmetic circuits since they can be evaluated over encoded inputs, where the evaluator may not know the underlying ring, and the evaluation is independent of the encoding parameters' underlying ring.

\begin{definition}[(Strongly) Ring-Independent Arithmetic Circuit]
An arithmetic circuit $\Cir$ with addition, subtraction and multiplication gates and with constants in in $\zo$ is ring-independent if there exists a boolean function $\func: \zo^n \rightarrow \zo$ such that for every ring $R$ and for every input $\xinp \in \zo^n$ we have that $\Cir(\xinp )=\func(\xinp)$ when $\Cir$ is evaluated over $R$. In this case we say that the circuit $\Cir$ computes the boolean function $\func$.

We say that $\Cir$ is {\em strongly} ring-independent the sub-circuit computing any internal wire in $\Cir$ is ring-independent.
\end{definition}

\begin{fact}
There exists a constant $c$ such that for every boolean circuit $\Cir$ there exists a strongly ring-independent arithmetic circuit $\Cir'$ computing $\Cir$ such that $|\Cir'| \leq c \cdot |\Cir|$. \guy{Note that we can maintain depth, log-space uniformity}
\end{fact}

\begin{fact}\label{fct.riac}
Let $\func,\gfunc$ be a pair of ring-independent arithmetic circuits on $n$ inputs.
\begin{enumerate}
\item
The circuit computing $\func \cdot \gfunc$ is ring independent.
\item
If for every $\vxinp \in \zo^n$, at least one of the two values $\func(\vxinp),\gfunc(\vxinp)$ is zero, then $\func + \gfunc$ is ring independent.
\end{enumerate}
\end{fact}

\guy{Do we need a subtraction property too?}
\omer{Don't think so. So far this fact is only used to argue that the multi-linear extension can be computed in a ring independent way.}
\subsection{Multi-linear Extension.}\label{sec.MLE}

For a boolean function $\func: \zo^n \rightarrow \zo$ and a ring $R$, we define the multi-linear extension $\tilde \func_R$, a multi-linear polynomial that agrees with $\func$ on all inputs in $\zo^n$. We show how to compute $\tilde \func_R$ over any ring $R$ using a single ring-independent circuit (this circuit always agrees with $f$ over the hypercube, but its values outside the hypercube may and will vary from ring to ring).

Let $\Iden_n$ be a ring-independent, multi-linear arithmetic circuit with $2n$ inputs described by the following arithmetic expression:
$$\Iden_n(\xinp_1,\dots,\xinp_n,\yinp_1,\dots,\yinp_n) = \prod_{i\in[n]}{\xinp_i\yinp_i + (1-\xinp_i)(1-\yinp_i)}\enspace.$$
observe that $\Iden_n$ computes the identity function over input pairs from the hypercube. For every $\vxinp,\vyinp \in \zo^n$, $\Iden_n(\vxinp,\vyinp) = 1$ iff $\vxinp = \vyinp$.

The the multi-linear extension $\tilde \func_R$ is defined by the following ring-independent, multi-linear arithmetic circuit:
\begin{align}\label{eq.mle}
\tilde \func(\vxinp) = \sum_{\vyinp \in \zo^n}{\Iden_n(\vxinp,\vyinp) \cdot \func(\vyinp)}\enspace.
\end{align}
Since for every $\vxinp \in \zo^n$ there exist only one value of $\vyinp \in \zo^n$ such that $\Iden_n(\vxinp,\vyinp) \neq 0$, it follows by \fctref{fct.riac} that $\tilde \func$ is a ring-independent arithmetic circuit computing $\func$.
%Since $\tilde \func$ is also multi-linear, it follows by the uniqueness of $\tilde \func_R$ that $\tilde \func$, when evaluated over $R$, is %equivalent to $\tilde \func_R$.

\guy{Commented out the references to uniqueness. I'm not sure what happens with polynomials over a general ring. In particular, is the multi-linear extension unique? We don't need the uniqueness for anything, so we can just define this as the multilinear extension over a general ring, which is what I did.}\omer{I need to make sure uniqueness is not used in the proof of the BB protocol.}

\section{A Non-Interactive Sum-Check Sub-Protocol.}
\label{sec.sc}

This section describes a non-interactive sum-check sub-protocol $(\scGen,\scP,\scV)$.
Let $n \in \Nat$ be a security parameter. Let $\edegree = \edegree(n), \level = \level(n)$ be polynomials and let:
$$\pp \gets \InstGen(1^n, \level, \edegree)\enspace,$$
be public parameters for a graded encoding scheme. Let $\zp$ be the field defined by $\pp$.
The sum-check sub-protocol depends on the public parameters $\pp$, and the soundness of protocol holds only for honestly generated parameters.
Let:
$$\func: \zp^\lleny \times \zp^\llenz \rightarrow \zp \enspace,$$
be a multi-variate low degree polynomial (represented as an arithmetic circuit).

Roughly speaking, the sum-check sub-protocol takes as input $\vzinp \in \zp^\lleny, \vval \in \zp$ and outputs $\vwinpo \in \zp^\llenz, \vvalo \in \zp$ such that, when the verifier accepts, she is guaranteed that if the input specified a false claim, then the output also specifies a false claim:
$$\quad \vval \neq \sum_{\vwinp \in \zo^\llenz}{\func(\vzinp,\vwinp)} \enspace \Rightarrow \vvalo \neq \func(\vzinp,\vwinpo) \quad$$

The inputs and outputs of the sum-check sub-protocol are encoded under the public parameters $\pp$.
The parameter $\mvarsy$ describe the number of dimensions used in the levels of input encodings. The parameter $\mvarsz$ describes the number of additional dimensions used internally within the protocol. In particular, the level of each input encoding is smaller than $\delta \cdot \slevel_{m_1}$, and the levels of each encoding computed internally and of each output encoding is smaller than $\delta \cdot \slevel_{m_1+m_2}$. In particular, note that it can (and will) be the case that $m_1 > \ell_1$ (or vice versa, depending on the given input), but it will (always) be the case that $m_2 = \ell_2$.


\subsection{Interface}
In this section we define the interfaces of the protocol and formulate its soundness property.

\subsubsection{The challenge generation procedure $\scGen$}
\paragraph{Input:}
\begin{enumerate}
    \item A security parameter $1^n$ and parameters $\mvarsy,\mvarsz$.
    \item Public parameters for a graded encoding:
    $$\pp \gets \InstGen(1^n, \level, \edegree)\enspace,$$
    including encodings of the constants $\zo$. We require that $\level \geq \mvarsy + \mvarsz$.
\end{enumerate}

\paragraph{Output:} A challenge $\CRS$.

\paragraph{Complexity:} The running time of $\scGen$ is $\poly(n)$. The challenge $\CRS$ is of length $m_2 \cdot \poly(n)$.

\subsubsection{The prover $\scP$}
\paragraph{Input:}
\begin{enumerate}
    \item The public parameters $\pp$.
    \item The challenge $\CRS$.
    \item An arithmetic circuit $\func$ taking $\lleny+\llenz$ inputs. $\func$ should contain only addition subtraction and multiplication gates and use only the constants $\zo$. $\func$ should be of individual degree at most $\edegree$ in every variable. We also require that $\ell_2 = m_2$ (for the $\scGen$ procedure's input $m_2$).
    \item An encoded input:
    $$\ins = \(\set{\enc{\zinp_i}{\vlevel_i}}_{i \in [\lleny]}, \enc{\vval}{\vlevel}\)\enspace,$$
    where $\vlevel$ and $\set{\vlevel_i}_{i \in [\lleny]}$ are levels in $\Lambda(\level,\edegree)$ such that:
    $$\sum_{i \in [\lleny]}{\edegree_i \cdot \vlevel_i} = \vlevel \leq \edegree \cdot \slevel_{\mvarsy}\enspace,$$
    where $\edegree_i$ is the individual degree of $\func$ in its $i$-th input variable.
\end{enumerate}

\paragraph{Output:}
\begin{enumerate}
    \item
    An encoded output:
    $$\inso = \(\vwinpo = \set{\enc{\winpo_i}{\elevel_{\mvarsy + i}}}_{i\in [\llenz]},\enc{\vvalo}{\vlevel + \ulevel}\)\enspace,$$
    where:
    $$\ulevel = \sum_{j \in [\llenz]}{\edegree \cdot \elevel_{\mvarsy + j}}\enspace.$$
    \item
    A proof $\Proof$ for the fact that:
    $$\vval \neq \sum_{\vwinp \in \zo^\llenz}{\func(\vzinp,\vwinp)} \quad \Rightarrow \quad  \vvalo \neq \func(\vzinp,\vwinpo) \enspace.$$
\end{enumerate}

\paragraph{Complexity:} The running time of $\scP$ is $\poly(n,|\func|,2^{\ell_2})$. The proof $\Proof$ is of length $\delta \cdot \ell_2 \cdot \poly(n)$.

\subsubsection{The verifier $\scV$}
\paragraph{Input:}
\begin{enumerate}
    \item The public parameters $\pp$.
    \item The challenge $\CRS$.
    \item The encoded input $\ins$.
    \item The encoded output $\inso$.
    \item The proof $\Proof$.
\end{enumerate}

\paragraph{Output:} $1$ if the proof is accepted and $0$ otherwise.

\paragraph{Complexity:} The running time of $\scV$ is $\delta \cdot \ell_2 \cdot \poly(n)$.

\subsubsection{Completeness and Soundness}
The protocol's completeness and soundness properties are captured by the following claims:

\guy{add Completeness. Both the fact about the output and the fact that the verifier accepts}

\begin{claim}[Adaptive Soundness]\label{clm.scas}
for every pair of poly-size circuits $\cPins, \cPproof$ there exists a negligible function $\mu$ such that for every $n \in \Nat$:
$$\Pr\[
    \begin{array}{l}
        \pp \gets \InstGen(1^n, \level, \edegree);\\
        \CRS \gets \scGen(1^n,\pp,(\mvarsz,\mvarsy)); \\
        \func, \ins \gets \cPins(\pp,\CRS);\\
        \insc ,\cProof \gets \cPproof(\pp,\CRS,\func, \ins); \\
        1 \gets \scV(\pp,\CRS , \ins , \insc, \cProof);\\
        \Echeat
    \end{array}
\] \leq \mu(n)\enspace.$$
where:
$$\ins = \(\set{\enc{\zinp_i}{\vlevel_i}}_{i \in [\lleny]}, \enc{\vval}{\vlevel}\) \quad,\quad \insc = \( \vwinpc^* \set{\enc{\winpc_i}{\elevel_{\mvarsy + i}}}_{i\in [\llenz]},\enc{\vvalc}{\vlevel + \ulevel}\)\enspace,$$
\omer{what is going on above?} and $\Echeat$ is the event that:
$$\vval \neq \sum_{\vwinp \in \zo^\llenz}{\func(\vzinp,\vwinp)} \quad \wedge \quad  \vvalc = \func(\vzinp,\vwinpc) \enspace,$$
where the arithmetic, as well as the evaluation of $\func$ are over field $\zp$ underlying $\pp$.
\end{claim}

\begin{remark}
Similarly to Remark \ref{remark.falsifiable1}, observe that the event $\Echeat$ can be tested in polynomial time using the public parameters $\pp$, and using the operations $\Enc,\Add,\Sub,\Mult,\isZero$ on the input and output encodings $\ins, \inso$. For simplicity of presentation we define the event $\Echeat$ as a condition on the values:
$$\vzinp,\vwinpc,\vval,\vvalc\enspace,$$
(which cannot be efficiently computed from the input and output encoding), rather than explicitly describing the efficient testing procedure.
\end{remark}


\subsection{Construction} \label{sec.sc_con}
In this section we specify the strategies $\scGen,\scP$ and $\scV$.

\subsubsection{The challenge generation procedure $\scGen$}

Given the public parameters $\pp$ for the graded encoding scheme and the parameters $\mvarsy,\mvarsz$, $\scGen$ uses the functions $\Samp,\Enc$ to obtain the set of encodings:
    $$\CRS = \set{\enc{\relm_i}{\elevel_{\mvarsy + i}}}_{i \in [\llenz]} \enspace,$$
where $\relm_1,\dots,\relm_\mvarsz$ are independently uniform elements in $\zp$ (the field defined by $\pp$).
$\scGen$ outputs $\CRS$.

\subsubsection{The prover $\scP$}

Recall that the prover's input includes the public parameters $\pp$, the arithmetic circuit $\func$, the encoded input $\ins$ and the challenge $\CRS$, where:
$$\ins = \(\set{\enc{\zinp_i}{\vlevel_i}}_{i \in [\lleny]}, \enc{\vval}{\vlevel}\)\enspace.$$
$$\CRS = \set{\enc{\relm_i}{\elevel_{\mvarsy + i}}}_{i\in [\llenz]}\enspace.$$

\noindent In what follows the arithmetic is over $\zp$.

For the elements $\zinp_1,\dots,\zinp_{\lleny}$ defined by the input encoding, and for the elements $\relm_1,\dots,\relm_{i-1}$ defined by the encodings in $\CRS$, let $\gfunc_i$ be the univariate polynomial:
    $$\gfunc_i(\xi) = \sum_{\winp_{i+1},\dots,\winp_\llenz \in \zo}{\func(\zinp_1,\dots,\zinp_{\lleny}, \relm_1,\dots,\relm_{i-1},\xi,\winp_{i+1},\dots,\winp_\llenz)}\enspace,$$
and let $\set{\gfunc_{i,j}}_{j \in [0,\delta]}$ be the coefficients of $\gfunc_i$:
\begin{align}\label{eq.decompose_gi}
    \gfunc_i(\xi) = \sum_{j=0}^\delta g_{i,j} \cdot \xi^j.
\end{align}
The proof consists of the encodings of these coefficients:
    $$\Proof = \set{\enc{\gfunc_{i,j}}{\vlevel + \ulevel_i}}_{i \in [\llenz], j \in [0,\edegree]}\enspace,$$
where:
%GR1$$\ulevel_i = \sum_{i' \in [i]}{\edegree \cdot \elevel_{\mvarsy + i'}}\enspace.$$
$$\ulevel_i = \sum_{i' \in [1,i-1]}{\edegree \cdot \elevel_{\mvarsy + i'}}\enspace.$$
See below on how the prover computes these encoding. The output encodings are:
$$\inso = \(\set{\enc{\winpo_i}{\elevel_{\mvarsy + i}}}_{i\in [\llenz]},\enc{\vvalo}{\vlevel + \ulevel}\)\enspace,$$
where:
$$\winpo_i = \relm_i \quad,\quad \vvalo = \func(\vzinp,\winpo_1,\dots,\winpo_\llenz)\enspace.$$
$\scP$ outputs the encodings $\inso$ and the proof $\Proof$.

To compute the encodings of $\set{\gfunc_{i,j}}$ in the proof $\Proof$, we use arithmetic circuits $\set{\func_{i,j}}_{i \in [\llenz], j \in [0,\edegree]}$ taking $\lleny+\llenz-1$ inputs, such that:
$$\func(\vzinp, \vwinp) = \sum_{j \in [0,\edegree]}{\func_{i,j}(\vzinp, \winp_1,\dots \winp_{i-1},\winp_{i+1},\dots,\winp_\llenz) \cdot \winp_{i}^j}\enspace.$$
Note that a circuit for $\func_{i,j}$ is of degree $\edegree_i$ in the $i$-th variable, and can be efficiently computed from $f$.\guy{Footnote with reference about this} Now observe that:
\begin{align}\label{eq.sc_gij}
    \gfunc_{i,j} = \sum_{\winp_{i+1},\dots,\winp_\llenz \in \zo}{\func_{i,j}(\zinp_1,\dots,\zinp_{\lleny}, \relm_1,\dots,\relm_{i-1},\winp_{i+1},\dots,\winp_\llenz)}\enspace.
\end{align}
And indeed Equation \ref{eq.decompose_gi} holds. Following \eqnref{eq.sc_gij}, and using the circuit for $\func_{i,j}$ and the operations $\Enc,\Add,\Sub,\Mult$ on the input encodings and the encoding in $\CRS$



\subsubsection{The verifier $\scV$}
\paragraph{Input:}
\begin{enumerate}
    \item The public parameters $\pp$ including encodings of the constants $\zo$.
    \item The challenge:
    $$\CRS = \set{\enc{\relm_i}{\elevel_{\mvarsy + i}}}_{i\in [\llenz]}\enspace.$$
    \item The encoded input:
    $$\ins = \(\set{\enc{\zinp_i}{\vlevel_i}}_{i \in [\lleny]}, \enc{\vval}{\vlevel}\)\enspace.$$
    \item The encoded output:
    $$\inso = \(\set{\enc{\winpo_i}{\elevel_{\mvarsy + i}}}_{i\in [\llenz]},\enc{\vvalo}{\vlevel + \ulevel}\)\enspace,$$
    \item The proof:
    $$\Proof = \set{\enc{\gfunc_{i,j}}{\vlevel + \ulevel_i}}_{i \in [\llenz], j \in [0,\edegree]}\enspace.$$
\end{enumerate}

\noindent Following \eqnref{eq.decompose_gi}, and using the operations $\Enc,\Add,\Sub,\Mult$ on the input encodings, $\scV$ obtains:
    $$\set{\enc{\gfunc_{i}(\relm_i)}{\vlevel + \ulevel_i},\enc{\gfunc_{i}(0)+\gfunc_{i}(1)}{\vlevel + \ulevel_{i-1}}}_{i \in [\llenz]}\enspace,$$

Using the operations $\Sub, \isZero$ on the above encodings, the encodings in $\CRS$, and the input and output encodings, $\scV$ tests that:
\begin{align}
    \label{eq.sctest0}
    &&\vval &= \gfunc_1(0)+\gfunc_1(1) \\
    \label{eq.sctest1}
    \forall i \in [\llenz-1]&: &\gfunc_{i}(\relm_i) &= \gfunc_{i+1}(0)+\gfunc_{i+1}(1) \\
    \label{eq.sctest2}
    \forall i \in [\llenz]&: &\relm_i &= \winpo_i \\
    \label{eq.sctest3}
    &&\gfunc_{\llenz}(\relm_\llenz) &= \vvalo
\end{align}
$\scV$ accepts iff all tests pass.

\subsection{Soundness: Proof of \clmref{clm.scas}}
Assume towards contradiction that there exists a pair of poly-size circuits $(\cPins, \cPproof)$ and a polynomial $\Poly$ such that for infinitely many values of $n\in \Nat$, the event $\Echeat$ occurs with probability at least $\frac{1}{\Poly(n)}$. Fix such $n$. We show that there exist an adversary $\Adv_i$ that wins the security game in \assref{ass.assumption1} with probability $\frac{1}{\Poly(n)\cdot\llenz}$.
For every $i \in [\llenz]$, consider the adversary $\Adv_i$ that gets public parameters $\pp$ and an encoding $\enc{\relm}{\elevel_{\mvarsy + i}}$ of a random element $\relm$. $\Adv_i$ starts by emulating the procedure $\scGen(1^n,\pp)$ except that instead of sampling the encoding $\enc{\relm_i}{\elevel_{\mvarsy+ i}}$ on its own, it uses $\enc{\relm}{\elevel_{\mvarsy+ i}}$. That is, $\Adv_i$ obtains the encodings:
$$\CRS = \set{\enc{\relm_1}{\elevel_{\mvarsy+1}} , \dots,\enc{\relm_{i-1}}{\elevel_{\mvarsy+i-1}} , \enc{\relm}{\elevel_{\mvarsy+ i}} , \enc{\relm_{i+1}}{\elevel_{\mvarsy+i+1}} , \dots , \enc{\relm_\mvarsz}{\elevel_{\mvarsy+\llenz}}}\enspace.$$
Note that the $\CRS$ is distributed exactly as the output of $\scGen(1^n,\pp)$.
Next, $\Adv_i$ executes $\cPins(\pp,\CRS)$ and obtains:
$$\func \quad,\quad \ins = \(\set{\enc{\zinp_i}{\vlevel_i}}_{i \in [\lleny]}, \enc{\vval}{\vlevel}\)\enspace.$$
$\Adv_i$ then executes $\cPproof(\pp,\CRS,\func,\ins)$ and obtains output encodings and a proof:
$$\insc = \(\set{\enc{\winpc_i}{\elevel_{\mvarsy + i}}}_{i\in [\llenz]},\enc{\vvalc}{\vlevel + \ulevel}\) \quad,\quad \cProof = \set{\enc{\gfunc^*_{i,j}}{\vlevel + \ulevel_i}}_{i \in [\llenz], j \in [0,\edegree]} \enspace.$$
$\Adv_i$ also executes the honest prover $\scP(\pp,\CRS,\func,\ins)$ and obtains output encodings and a proof:
$$\inso = \(\set{\enc{\winpo_i}{\elevel_{\mvarsy + i}}}_{i\in [\llenz]},\enc{\vvalo}{\vlevel + \ulevel}\) \quad,\quad \Proof = \set{\enc{\gfunc_{i,j}}{\vlevel + \ulevel_i}}_{i \in [\llenz], j \in [0,\edegree]} \enspace.$$
Next, $\Adv_i$ uses the operation $\Sub, \isZero$ to find the maximal pair of indexes $(i',j) \in [\llenz] \times [0,\edegree]$ in lexicographical order such that $\gfunc^*_{i',j} \neq \gfunc_{i',j}$. If no such indexes are found or if $i' \neq i$, $\Adv_i$ aborts. Otherwise, $\Adv_i$ uses the functions $\Enc,\Add,\Sub,\Mult$ on the encodings in $\CRS,\Proof,\cProof$ to obtain:
$$\enc{\beta}{\vlevel+\ulevel_i} \quad,\quad \enc{\gamma}{\vlevel+\ulevel'_i} \enspace,$$
where
$$\beta = \gfunc^*_{i,j} - \gfunc_{i,j} \quad,\quad \gamma = \sum_{j' < j}{(\gfunc_{i,j'}-\gfunc^*_{i,j'})\relm_{i}^{j'}}\enspace,$$
and
%GR1$$\ulevel'_i= \ulevel'_{i-1} + (j-1)\cdot \elevel_{\mvarsy+i}\enspace.$$
$$\ulevel'_i= \ulevel_{i} + (j-1)\cdot \elevel_{\mvarsy+i}\enspace.$$
Note that indeed:
$$j \cdot \elevel_{\mvarsy+i} \not\leq \vlevel + \ulevel'_i \enspace.$$
Finally $\Adv_i$ outputs $\enc{\beta}{\vlevel+\ulevel_i},\enc{\gamma}{\vlevel+\ulevel'_i}$.
\guy{in the above, I changed the level of $\beta$ and the definition of $\ulevel_i'$, please check (old versions commented out)} \omer{Not sure what is going on. Let talk about this.}


Next we prove that for some $i \in [\llenz]$, $\Adv_i$ wins the security game in \assref{ass.assumption1} with probability $\frac{1}{\Poly(n)\cdot\llenz}$. For $i \in [\llenz]$ let:
$$\gfunc^*_i(\xi) = \sum_{j \in [0,\edegree]}{\gfunc^*_{i,j} \cdot \xi^j} \quad,\quad \gfunc_i(\xi) = \sum_{j \in [0,\edegree]}{\gfunc_{i,j} \cdot \xi^j}\enspace,$$
and let $E_i$ be that event that $\gfunc^*_i \not\equiv \gfunc_i$.

Conditioned on the event $\Echeat$ we have that:
$$\sum_{\vwinp \in \zo^\llenz}{\func(\vzinp,\vwinp)} = \gfunc_1(0) + \gfunc_1(1) \neq \vval \enspace.$$
Conditioned on the event $\Echeat$, we also have that and that the verifier's Test~\ref{eq.sctest0} passes and
$$\gfunc^*_1(0) + \gfunc^*_1(1) = \vval \enspace.$$
Therefore, $\gfunc^*_1 \not\equiv \gfunc_1$, and the event $E_1$ must hold. Thus, $\Adv_i$ finds some (maximal) indices $(i',j)$ as described above.

Let $G_i$ be the event that $\Echeat$ occurs and that $i' = i$ (that is, $\Adv_i$ does not abort).
Conditioned on $G_i$, $i=i'$ is the maximal index such that $E_i$ holds. Therefore, in the case that $i<\llenz$ we have that $\neg E_{i+1}$ holds, and since the verifier's Test~\ref{eq.sctest1} passes we have that:
$$\gfunc^*_{i}(\relm_{i}) = \gfunc^*_{i+1}(0) + \gfunc^*_{i+1}(1) = \gfunc_{i+1}(0) + \gfunc_{i+1}(1)  = \gfunc_{i}(\relm_{i})\enspace.$$
In the case that $i = \llenz$ we have that conditioned on $G_i$:
\begin{align}
\label{eq.scp1}
\gfunc^*_{\llenz}(\relm_{\llenz}) &=
\vvalc \\
\label{eq.scp2}
&= \func(\vzinp,\vwinpc) \\
\label{eq.scp3}
&= \func(\vzinp,\relm_1,\dots,\relm_{\llenz}) \\
\label{eq.scp4}
&= \func(\vzinp,\vwinpo)
= \vvalo
= \gfunc_{\llenz}(\relm_{\llenz})
\enspace,
\end{align}
where \eqref{eq.scp1} follows from the fact that the verifier's Test~\ref{eq.sctest3} passes, \eqref{eq.scp2} follows from the event $\Echeat$,\eqref{eq.scp3} follows from the fact that the verifier's Test~\ref{eq.sctest2} passes, and \eqref{eq.scp4} follows from the definition of the honest prove $\scP$. Overall, for every $i \in [\llenz]$, we conclude that if we condition on $G_i$, we have that:
$$\gfunc^*_i \not\equiv \gfunc_i \quad,\quad \gfunc^*_{i}(\relm_{i}) = \gfunc_{i}(\relm_{i})\enspace.$$
Thus
$$0 = \sum_{j' \in [0,\edegree]} (\gfunc_{i,j'} - \gfunc^*_{i,j'})\relm_{i}^{j'}.$$
Since $j$ is the maximal index such that $\gfunc^*_{i,j} \neq \gfunc_{i,j}$, we have that:
$$0 = \sum_{j' \in [0,j]} (\gfunc_{i,j'} - \gfunc^*_{i,j'})\relm_{i}^{j'} \implies (\gfunc^*_{i,j} - \gfunc_{i,j})\relm_{i}^{j} = \sum_{j' < j}{(\gfunc_{i,j'} - \gfunc^*_{i,j'})\relm_{i}^{j'}},$$
and we conclude that conditioned on $G_i$:
$$\beta \cdot \relm_{i}^{j} = (\gfunc^*_{i,j} - \gfunc_{i,j})\relm_{i}^{j} = \sum_{j' < j}{(\gfunc_{i,j'} - \gfunc^*_{i,j'})\relm_{i}^{j'}} = \gamma \enspace,$$
and $\beta \neq 0$. Hence, $\Adv_i$ wins the security game.

It is left to show that (for some $i \in [\llenz]$) the event $G_i$ occurs with noticeable probability.
Recall that the challenge $\CRS$ generated by $\Adv_i$ is distributed exactly as the output of $\scGen(1^n,\pp)$, and by our assumption, the event $\Echeat$ occurs in the execution of $\Adv_i$ with probability at least $\frac{1}{\Poly(n)}$. Conditioned on $\Echeat$, we know that $E_1$ occurs, and thus $G_{i'}$ occurs for some $i' \in [\llenz]$. Since the view of $\cPins$ and $\cPproof$ and the event $\Echeat$ are all independent of $i$, we conclude that conditioned on $\Echeat$, there exists $i \in [\llenz]$ such that the event $G$ occurs with probability at least $\frac{1}{\Poly(n)\cdot \llenz}$.


\section{A 2-to-1 Sub-Protocol.}
\label{sec.tto}

This section describes a 2-to-1 sub-protocol $(\ttoGen,\ttoP,\ttoV)$.
Let $n \in \Nat$ be a security parameter. Let $\edegree = \edegree(n), \level = \level(n)$ be polynomials and let:
$$\pp \gets \InstGen(1^n, \level, \edegree)\enspace,$$
be public parameters for a graded encoding scheme. Let $\zp$ be the field defined by $\pp$.
The 2-to-1 sub-protocol will depend on the public parameters $\pp$, and the soundness of protocol will only hold for honestly generated parameters.
Let:
$$\func: \zp^\llen\rightarrow \zp \enspace,$$
be a multi-linear polynomial (represented as an arithmetic circuit).

Roughly, the 2-to-1 sub-protocol takes as input $\vwinp^1,\vwinp^2 \in \zp^\llen, \vval^1,\vval^2 \in \zp$ and outputs $\vwinpo \in \zp^\llen, \vvalo \in \zp$ such that:
$$\func(\vwinpo) = \vvalo \quad \Rightarrow \quad  \func(\vwinp^1) = \vval^1 \quad \land \quad \func(\vwinp^2) = \vval^2 \enspace,$$
holds whenever the verifier accepts.

The inputs and outputs of the 2-to-1 sub-protocol are encoded under the public parameters $\pp$.
Let $\mvars$ be a parameter describing the levels used to encode the inputs and the levels used internally in the protocol. The first $\mvars$ coordinates of the level are used to encode the inputs, and the $(\mvars+1)$-th coordinate is used by the protocol.

\subsection{Interface}
In this section we define the interfaces of the protocol and formulate its soundness property.


\subsubsection{The challenge generation procedure $\ttoGen$}
\paragraph{Input:}
\begin{enumerate}
    \item A security parameter $1^n$ and a parameter $\mvars$.
    \item Public parameters for a graded encoding:
    $$\pp \gets \InstGen(1^n, \level, \edegree)\enspace,$$
    including encodings of the constants $\zo$. We require that $\level \geq \mvars + 1$ and that $\edegree \geq \mvars$.
\end{enumerate}

\paragraph{Output:} A challenge $\CRS$.

\subsubsection{The prover $\ttoP$}
\paragraph{Input:}
\begin{enumerate}
    \item The public parameters $\pp$.
    \item The challenge $\CRS$.
    \item A multi-linear arithmetic circuit $\func$ taking $\llen$ inputs. $\func$ should contain only addition subtraction and multiplication gates and use only the constants $\zo$.
    \item An encoded input:
    $$\ins = \(\set{\enc{\winp^1_i}{\vlevel_i},\enc{\winp^2_i}{\vlevel_i}}_{i \in [\llen]}, \enc{\vval^1}{\vlevel} , \enc{\vval^2}{\vlevel}\)\enspace,$$
    where $\vlevel$ and $\set{\vlevel_i}_{i \in [\llen]}$ are levels in $\Lambda(\level,\edegree)$ such that:
    $$\sum_{i \in [\lleny]}{\vlevel_i} = \vlevel \leq \edegree \cdot \slevel_{\mvars}\enspace.$$
\end{enumerate}

\paragraph{Output:}
\begin{enumerate}
    \item
    An encoded output:
    $$\inso = \(\set{\enc{\winpo_i}{\vlevel_i + \elevel_{\mvars + 1}}}_{i \in [\llen]}, \enc{\vvalo}{\vlevel + \llen \cdot \elevel_{\mvars + 1}}\)\enspace.$$
    \item
    A proof $\Proof$ for the fact that:
    $$\func(\vwinpo) = \vvalo \quad \Rightarrow \quad  \func(\vwinp^1) = \vval^1 \quad \land \quad \func(\vwinp^2) = \vval^2 \enspace.$$
\end{enumerate}

\subsubsection{The verifier $\ttoV$}
\paragraph{Input:}
\begin{enumerate}
    \item The public parameters $\pp$.
    \item The challenge $\CRS$.
    \item The encoded input $\ins$.
    \item The encoded output $\inso$.
    \item The proof $\Proof$.
\end{enumerate}

\paragraph{Output:} $1$ if the proof is accepted and $0$ otherwise.

\subsubsection{Soundness}
The soundness of the protocol is captured by the following claim:
\begin{claim}[Adaptive Soundness]\label{clm.ttoas}
for every pair of poly-size circuits $\cPins, \cPproof$ there exists a negligible function $\mu$ such that for every $n \in \Nat$:
$$\Pr\[
    \begin{array}{l}
        \pp \gets \InstGen(1^n, \level, \edegree);\\
        \CRS \gets \ttoGen(1^n,\pp,\mvars); \\
        \func, \ins \gets \cPins(\pp,\CRS);\\
        \insc,\cProof \gets \cPproof(\pp,\CRS,\func, \ins); \\
        1 \gets \ttoV(\pp,\CRS , \ins ,\insc, \cProof);\\
        \Echeat
    \end{array}
\] \leq \mu(n)\enspace.$$
where:
$$\ins = \(\set{\enc{\winp^1_i}{\vlevel_i},\enc{\winp^2_i}{\vlevel_i}}_{i \in [\llen]}, \enc{\vval^1}{\vlevel} , \enc{\vval^2}{\vlevel}\) \quad,\quad \insc = \(\set{\enc{\winpc_i}{\vlevel_i + \elevel_{\mvars + 1}}}_{i \in [\llen]}, \enc{\vvalc}{\vlevel + \llen \cdot \elevel_{\mvars + 1}}\)\enspace,$$
and $\Echeat$ is the event that:
$$\func(\vwinpc) = \vvalc \quad\not\rightarrow\quad \( \func(\vwinp^1) = \vval^1 \quad \land \quad \func(\vwinp^2) = \vval^2\) \enspace,$$
where $\func$ is evaluated over the field $\zp$ defined by $\pp$.
\end{claim}

\begin{remark}
Note that the event $\Echeat$ can be tested in polynomial time using the public parameters $\pp$, and using the operations $\Enc,\Add,\Sub,\Mult,\isZero$ on the input and output encodings $\ins, \inso$. For simplicity of presentation we define the event $\Echeat$ as a condition on the values:
$$\vwinp^1, \vval^1, \vwinp^2, \vval^2, \vwinpc, \vvalc\enspace,$$
(that cannot be efficiently computed from the input and output encoding) instead of explicitly describing the efficient testing procedure.
\end{remark}

\subsection{Construction} \label{sec.tto_con}
In this section we specify the strategies $\ttoGen,\ttoP$ and $\ttoV$.

\subsubsection{The challenge generation procedure $\ttoGen$}
Given the public parameters $\pp$ for the graded encoding scheme and the parameter $\mvars$, $\ttoGen$ uses the functions $\Samp,\Enc$ to obtain the encoding:
    $$\CRS = \enc{\telm}{\elevel_{\mvars + 1}}\enspace,$$
where $\telm$ is a uniform elements in $\zp$ (the field defined by $\pp$).
$\ttoGen$ outputs $\CRS$.

\subsubsection{The prover $\ttoP$}
\paragraph{Input:}
\begin{enumerate}
    \item The public parameters $\pp$.
    \item The challenge:
    $$\CRS = \enc{\telm}{\elevel_{\mvars + 1}}\enspace.$$
    \item The arithmetic circuit $\func$ taking $\llen$ inputs. $\func$ should contain only addition subtraction and multiplication gates and use only the constants $\zo$. $\func$ should be multi-linear.
    \item The encoded input:
    $$\ins = \(\set{\enc{\winp^1_i}{\vlevel_i},\enc{\winp^2_i}{\vlevel_i}}_{i \in [\llen]}, \enc{\vval^1}{\vlevel} , \enc{\vval^2}{\vlevel}\)\enspace,$$
    where $\vlevel$ and $\set{\vlevel_i}_{i \in [\llen]}$ are levels in $\Lambda(\level,\edegree)$ such that:
    $$\sum_{i \in [\lleny]}{\vlevel_i} = \vlevel \leq \edegree \cdot \slevel_{\mvars}\enspace.$$
\end{enumerate}

\noindent Let $\zline(\xinp)$ be the line:
$$\zline(\xinp) = \xinp \cdot \vwinp^1 + (1 - \xinp) \cdot \vwinp^2\enspace,$$
that is, for every $i \in [\llen]$:
\begin{align}\label{eq.tto_line}
\zline(\xinp)[i] = \xinp \cdot \winp^1_i + (1 - \xinp) \cdot \winp^2_i\enspace.
\end{align}
Let $\gfunc(\xinp)$ be the univariate polynomial:
$$\gfunc(\xinp) = \func(\zline(\xinp))\enspace.$$
Since $\func$ is multi-linear, $\gfunc$ is of degree $\llen$.
For every $j \in [0,\llen]$ let $\gfunc_j$ be the field element such that:
\begin{align}\label{eq.tto_gi}
\gfunc(\xinp) = \sum_{j \in [0,\llen]}{\gfunc_j \cdot \xinp^j}\enspace.
\end{align}

Given the circuit of $\func$, and using the operation $\Enc,\Add,\Sub,\Mult$ on the input encodings, $\ttoP$ obtains the encodings:
$$\Proof = \set{\enc{\gfunc_j}{\vlevel}}_{j \in [0,\llen]}\enspace.$$
Using also the encoding in $\CRS$, $\ttoP$ obtains the output encoding:
$$\inso = \(\set{\enc{\winpo_i}{\vlevel_i + \elevel_{\mvars + 1}}}_{i \in [\llen]}, \enc{\vvalo}{\vlevel + \llen \cdot \elevel_{\mvars + 1}}\)\enspace,$$
where:
$$\winpo_i = \zline(\telm)[i] \quad,\quad \vvalo = \gfunc(\telm)\enspace.$$

$\ttoP$ outputs the proof $\Proof$ and the output encoding $\inso$.

\subsubsection{The verifier $\ttoV$}
\paragraph{Input}
\begin{enumerate}
    \item The public parameters $\pp$ including encodings of the constants $\zo$.
    \item The challenge:
    $$\CRS = \enc{\telm}{\elevel_{\mvars + 1}}\enspace.$$
    \item The encoded input:
    $$\ins = \(\set{\enc{\winp^1_i}{\vlevel_i},\enc{\winp^2_i}{\vlevel_i}}_{i \in [\llen]}, \enc{\vval^1}{\vlevel} , \enc{\vval^2}{\vlevel}\)\enspace,$$
    where $\vlevel$ and $\set{\vlevel_i}_{i \in [\llen]}$ are levels in $\Lambda(\level,\edegree)$ such that:
    $$\sum_{i \in [\lleny]}{\vlevel_i} = \vlevel \leq \edegree \cdot \slevel_{\mvars}\enspace.$$
    \item The encoded output:
    $$\inso = \(\set{\enc{\winpo_i}{\vlevel_i + \elevel_{\mvars + 1}}}_{i \in [\llen]}, \enc{\vvalo}{\vlevel + \llen \cdot \elevel_{\mvars + 1}}\)\enspace.$$
    \item The proof:
    $$\Proof = \set{\enc{\gfunc_j}{\vlevel}}_{j \in [0,\llen]}\enspace.$$
\end{enumerate}

\noindent Following Equations~\ref{eq.tto_line},\ref{eq.tto_gi}, and using the operations $\Enc,\Add,\Sub,\Mult$ on the input encodings, $\ttoV$ obtains:
\begin{align*}
\begin{array}{c}
\set{\enc{\zline(\telm)[i]}{\vlevel_i + \elevel_{\mvars + 1}} \quad,\quad \enc{\zline(0)[i]}{\vlevel_i} \quad,\quad \enc{\zline(1)[i]}{\vlevel_i}}_{i \in [\llen]} \\
\enc{\gfunc(\telm)}{\vlevel + \llen \cdot \elevel_{\mvars + 1}} \quad,\quad\enc{\gfunc(0)}{\vlevel} \quad,\quad\enc{\gfunc(1)}{\vlevel} \enspace.
\end{array}
\end{align*}

Using the operations $\Sub, \isZero$ on the above encodings, and the input encodings, $\ttoV$ tests that:
\begin{align*}
    \forall i \in [\llenz]&: &\zline(\telm)[i] &= \winpo_i & \zline(0)[i] &= \winp^2_i & \zline(1)[i] &= \winp^1_i \\
    &&\gfunc(\telm) &= \vvalo & \gfunc(0) &= \vval^2 & \gfunc(1) &= \vval^1
\end{align*}
$\ttoV$ accepts iff all tests pass.


\subsection{Proof of \clmref{clm.ttoas}}
Assume towards contradiction that there exists a pair of poly-size circuits $(\cPins, \cPproof)$ and a polynomial $\Poly$ such that for infinitely many values of $n\in \Nat$, the event $\Echeat$ occurs with probability at least $\frac{1}{\Poly(n)}$. Fix such $n$. We show that there exist an adversary $\Adv$ that wins the security game in \assref{ass.assumption1} with probability $\frac{1}{\Poly(n)}$.
Consider the adversary $\Adv$ that gets public parameters $\pp$ and an encoding $\enc{\telm}{\elevel_{\mvars + 1}}$ of a random element $\telm$. $\Adv$ first obtains a the challenge:
$$\CRS = \enc{\telm}{\elevel_{\mvars+1}}\enspace.$$
Note that $\CRS$ is distributed exactly as the output of $\ttoGen(1^n,\pp)$.
Next, $\Adv$ executes $\cPins(\pp,\CRS)$ and obtains:
$$\func \quad,\quad \ins = \(\set{\enc{\winp^1_i}{\vlevel_i},\enc{\winp^2_i}{\vlevel_i}}_{i \in [\llen]}, \enc{\vval^1}{\vlevel} , \enc{\vval^2}{\vlevel}\)\enspace.$$
$\Adv$ then executes $\cPproof(\pp,\CRS,\func,\ins)$ and obtains output encodings and a proof:
$$\insc = \(\set{\enc{\winpc_i}{\vlevel_i + \elevel_{\mvars + 1}}}_{i \in [\llen]}, \enc{\vvalc}{\vlevel + \llen \cdot \elevel_{\mvars + 1}}\) \quad,\quad \Proof = \set{\enc{\gfunc^*_j}{\vlevel}}_{j \in [0,\llen]}\enspace.$$
$\Adv$ also executes the honest prover $\ttoP(\pp,\CRS,\func,\ins)$ and obtains output encodings and a proof:
$$\inso = \(\set{\enc{\winpo_i}{\vlevel_i + \elevel_{\mvars + 1}}}_{i \in [\llen]}, \enc{\vvalo}{\vlevel + \llen \cdot \elevel_{\mvars + 1}}\) \quad,\quad \Proof = \set{\enc{\gfunc_j}{\vlevel}}_{j \in [0,\llen]}\enspace.$$
Next, $\Adv$ uses the operation $\Sub, \isZero$, finds the maximal indexe $j \in [0,\llen]$ such that $\gfunc^*_j \neq \gfunc_j$. If no such index is found, $\Adv$ aborts. Otherwise, $\Adv$ uses the functions $\Enc,\Add,\Sub,\Mult$ on the encodings in $\CRS,\Proof,\cProof$ to obtain:
$$\enc{\beta}{\vlevel+(j-1)\cdot \elevel_{\mvars + 1}} \quad,\quad \enc{\gamma}{\vlevel+(j-1)\cdot \elevel_{\mvars + 1}} \enspace,$$
where:
$$\beta = \gfunc^*_j - \gfunc_j \quad,\quad \gamma = \sum_{j' < j}{(\gfunc_{j'}-\gfunc^*_{j'})\telm^{j'}}\enspace.$$
Note that indeed:
$$j \cdot \elevel_{\mvars + 1} \not\leq \vlevel+(j-1)\cdot \elevel_{\mvars + 1}\enspace.$$
Finally $\Adv$ outputs $\enc{\beta}{\vlevel+(j-1)\cdot \elevel_{\mvars + 1}},\enc{\gamma}{\vlevel+(j-1)\cdot \elevel_{\mvars + 1}}$.

Next we prove that $\Adv_i$ wins the security game in \assref{ass.assumption1} with probability $\frac{1}{2\Poly(n)}$. Let:
$$\gfunc^*(\xinp) = \sum_{j \in [0,\llen]}{\gfunc^*_j \cdot \xinp^j} \quad,\quad \gfunc(\xinp) = \sum_{j \in [0,\edegree]}{\gfunc_j \cdot \xinp^j}\enspace,$$
and let $E$ be that event that $\gfunc^*(\xinp) \not\equiv \gfunc(\xinp)$.
Conditioned on the event $\Echeat$ we have that:
$$\gfunc(1) = \func(\vwinp^1) \neq \vval^1 \quad \lor \quad \gfunc(0) = \func(\vwinp^2) \neq \vval^2 \enspace.$$
Conditioned on the event $\Echeat$ we also have that and that the verifier's tests pass and
$$\gfunc^*(1) = \vval^1 \quad \lor \quad \gfunc^*(0) = \vval^2 \enspace.$$
Therefore the event $E$ must hold and $\Adv$ must find an index $j$ as described.
Conditioned on the event $\Echeat$ we also have that:
\begin{align}
\label{eq.ttop1}
\gfunc^*(\telm) &=
\vvalc \\
\label{eq.ttop2}
&= \func(\vwinpc) \\
\label{eq.ttop3}
&= \func(\zline(\telm)[1], \dots, \zline(\telm)[\llen]) \\
\label{eq.ttop4}
&= \func(\vwinpo)
= \vvalo
= \gfunc_{\llenz}(\relm_{\llenz})
\enspace,
\end{align}
where \eqref{eq.ttop1} and \eqref{eq.ttop3} follow from the fact that the verifier's tests pass and \eqref{eq.ttop2} follows from the event $\Echeat$.

Overall we have that conditioned on $\Echeat$:
$$\gfunc^*(\xinp) \not\equiv \gfunc(\xinp) \quad,\quad \gfunc^*(\telm) = \gfunc(\telm)\enspace.$$
Therefore, since $j$ is the maximal index such that $\gfunc^*j \neq \gfunc_j$, we have that conditioned on $\Echeat$:
$$\beta \cdot \telm^{j} = (\gfunc^*_j - \gfunc_j)\telm^{j} = \sum_{j' < j}{(\gfunc_{j'} - \gfunc^*_{j'})\telm^{j'}} = \gamma \enspace,$$
and $\beta \neq 0$. Hence, $\Adv$ wins the security game.

Since the challenge $\CRS$ generated by $\Adv$ is distributed exactly as the output of $\scGen(1^n,\pp)$, and by our assumption, the event $\Echeat$ occurs in the execution of $\Adv$ with probability $\frac{1}{\Poly(n)}$.

\section{A Bare-Bones Delegation Sub-Protocol}\label{sec.bb}

This section describes a bare-bones delegation protocol $(\bbGen,\bbP,\bbV)$.
Let $n \in \Nat$ be a security parameter.
Let $\func$ be a layered fan-in 2, strongly ring-independent arithmetic circuit with $\inpS$ inputs.
Let $\cirS$ be the size of $\func$ and $\cirD$ be the depth of $\func$ and let $\mvars = \log(\cirS)$. (For simplicity and without loss of generality we assume that $\cirS$ is a power of 2.) We index every gate of $\func$ by a string in $\zo^\mvars$.
We number the layers of $\func$ such that layer $0$ is the output layer and layer $\cirD$ is the input layer.

For every $i \in [\cirD]$ let:
$$\Fadd_i,\Fsub_i,\Fmult_i: \zo^{3\mvars} \rightarrow \zo \enspace,$$
be functions such that $\Fadd_i(\gate_1,\gate_2,\gate_3) = 1$ if $\gate_1$ is a gate in layer $i-1$, $\gate_2,\gate_3$ are gates is in layer $i$ and $\gate_1$ is adding the output of $\gate_2$ and $\gate_3$. Otherwise $\Fadd_i(\gate_1,\gate_2,\gate_3) = 0$. $\Fsub_i$ and $\Fmult_i$ are defined similarly.
Let $\edegree$ be a degree parameter and let $\EFadd_i,\EFsub_i,\EFmult_i$ be ring-independent arithmetic circuits of degree $\edegree$ computing the functions $\Fadd_i,\Fsub_i,\Fmult_i$.

Roughly, bare-bones delegation protocol takes as input an input $\xinp$ for $\func$ and outputs ring elements:
$$\set{\vzinp_i,\vvala_i,\vvals_i,\vvalm_i}_{i \in [\cirD]} \enspace,$$
such that:
$$ \(\forall i \in [\cirD]:\(\EFadd_i(\vzinp_i) = \vvala_i\) \land \(\EFsub_i(\vzinp_i) = \vvals_i\) \land \(\EFmult_i(\vzinp_i) = \vvalm_i\)\) \quad \Rightarrow \quad \func(\xinp) = 1 \enspace,$$
holds whenever the verifier accepts.
The output elements of the bare-bones delegation protocol are encoded under some public parameters $\pp$ that are included in the protocol output, and the arithmetic above in over a field $\zp$ that is defined by $\pp$.

\subsection{Interface}
In this section we define the interfaces of the protocol and formulate its soundness property.


\subsubsection{The challenge generation procedure $\bbGen$}
\paragraph{Input:} A security parameter $1^n$ and parameters $\edegree,\mvars$.

\paragraph{Output:} A challenge $\CRS$.

\subsubsection{The prover $\bbP$}

\paragraph{Input:}
\begin{enumerate}
    \item The challenge $\CRS$.
    \item Ring-independent arithmetic circuits:
    $$\set{\EFadd_i,\EFsub_i,\EFmult_i}_{i \in \cirD}\enspace,$$
    each of degree $\edegree$, describing a layered, fan-in 2, ring-independent arithmetic circuit $\func$ of size $\cirS = 2^\mvars$, depth $\cirD$, and with $\inpS$ inputs.
    \item An input $\xinp \in \zo^\inpS$ to $\func$.
\end{enumerate}

\paragraph{Output:}
\begin{enumerate}
    \item
    Public parameters:
    $$\pp \gets \InstGen(1^n, \cirD \cdot \mvars', \max(\edegree + 3,\mvars))\enspace,$$
    where $\mvars' = 3\mvars + 1$

    \item
    An encoded output:
    $$\inso = \(\set{\enc{\winp_{i,j}}{\elevel_{(i-1) \cdot \mvars' + j}}}_{i \in [\cirD], j \in [\mvars'-1]} ,\set{\enc{\vvala_i}{\edegree \cdot \ulevel_i}, \enc{\vvals_i}{\edegree \cdot \ulevel_i}, \enc{\vvalm_i}{\edegree \cdot \ulevel_i}}_{i \in [\cirD]}\)\enspace,$$
    where for every $i \in [\cirD]$:
    $$\ulevel_i = \sum_{j \in [\mvars'-1]}{\elevel_{(i-1) \cdot \mvars' + j}}\enspace.$$
    \item
    A proof $\Proof$ for the fact that:
    $$ \(\forall i \in [\cirD]:\(\EFadd_i(\vwinp_i) = \vvala_i\) \land \(\EFsub_i(\vwinp_i) = \vvals_i\) \land \(\EFmult_i(\vwinp_i) = \vvalm_i\)\) \quad \Rightarrow \quad \func(\xinp) = 1 \enspace,$$
    where for every $i \in [\cirD]$:
    $$\vwinp_i = \(\winp_{i,1},\dots,\winp_{i,\mvars' -1}\)\enspace.$$

\end{enumerate}


\subsubsection{The verifier $\bbV$}
\paragraph{Input:}
\begin{enumerate}
    \item The challenge $\CRS$.
    \item The input $\xinp$.
    \item The public parameters $\pp$.
    \item The encoded output $\inso$.
    \item The proof $\Proof$.
\end{enumerate}

\paragraph{Output:} $1$ if the proof is accepted and $0$ otherwise.


\subsubsection{Soundness}
The soundness of the protocol is captured by the following claim:
\begin{claim}[Adaptive Soundness]\label{clm.bbas}
for every pair of poly-size circuits $\cPins, \cPproof$ there exists a negligible function $\mu$ such that for every $n \in \Nat$:
$$\Pr\[
    \begin{array}{l}
        \CRS \gets \bbGen(1^n,\edegree,\mvars); \\
        \func, \xinp \gets \cPins();\\
        \pp,\insc,\cProof \gets \cPproof(\CRS,\func, \xinp); \\
        1 \gets \bbV(\CRS, \xinp, \pp, \insc, \cProof);\\
        \Echeat
    \end{array}
\] \leq \mu(n)\enspace.$$
where $\func$ is given by the arithmetic circuits:
$$\set{\EFadd_i,\EFsub_i,\EFmult_i}_{i \in \cirD}\enspace,$$
and
$$\insc = \(\set{\enc{\winp_{i,j}}{\elevel_{(i-1) \cdot \mvars' + j}}}_{i \in [\cirD], j \in [\mvars'-1]} ,\set{\enc{\vvala_i}{\edegree \cdot \ulevel_i}, \enc{\vvals_i}{\edegree \cdot \ulevel_i}, \enc{\vvalm_i}{\edegree \cdot \ulevel_i}}_{i \in [\cirD]}\)\enspace,$$
and $\Echeat$ is the event that:
$$ \(\forall i \in [\cirD]:\(\EFadd_i(\vwinp_i) = \vvala_i\) \land \(\EFsub_i(\vwinp_i) = \vvals_i\) \land \(\EFmult_i(\vwinp_i) = \vvalm_i\)\) \quad\not\rightarrow\quad \func(\xinp) = 1 \enspace,$$
where for every $i \in [\cirD]$:
$$\vwinp_i = \(\winp_{i,1},\dots,\winp_{i,\mvars' -1}\)\enspace,$$
and the arithmetic is over the field $\zp$ that is defined by $\pp$.
\end{claim}

\begin{remark}
Note that the event $\Echeat$ can be tested in polynomial time using the public parameters $\pp$, using the arithmetic circuits:
$$\set{\EFadd_i,\EFsub_i,\EFmult_i}_{i \in \cirD}\enspace,$$
and using the operations $\Enc,\Add,\Sub,\Mult,\isZero$ on the output encodings $\inso$. For simplicity of presentation we define the event $\Echeat$ as a condition on the values:
$$\set{\vwinp_i,\vvala_i,\vvals_i,\vvalm_i}_{i \in [\cirD]} \enspace,$$
(that cannot be efficiently computed from the output encoding) instead of explicitly describing the efficient testing procedure.
\end{remark}


\subsection{Construction}
In this section we specify the strategies $\bbGen,\bbP$ and $\bbV$.

\subsubsection{The challenge generation procedure $\bbGen$}
$\bbGen$ is given the security parameter $1^n$ and the parameters $\edegree,\mvars$ and it is defined as follows:
\begin{enumerate}
\item
$\bbGen$ generates public parameters for a graded encoding scheme:
$$\pp \gets \InstGen(1^n, \cirD \cdot \mvars', \max(\edegree + 3,\mvars))\enspace,$$
where $\mvars' = 3\mvars + 1$. Let $\zp$ be the field defined by $\pp$.
\item
For every $i \in [\cirD]$, $\bbGen$ samples challenges $\scCRS^i,\ttoCRS^i$ for the sum-check and 2-to-1 sub-protocols (Sections \ref{sec.sc},\ref{sec.tto}). The $\cirD$ executions of the sub-protocols use encodings in different levels. Specifically, the level vector has $\cirD \cdot \mvars'$ coordinates, which we think of as divided into $\cirD$ groups of $\mvars'$ coordinates each. The $i$-th sum-check sub-protocol uses the first $\mvars' -1 = 3\mvars$ coordinates of the $i$-th group (the input is encoded in the previous coordinates). The $i$-th 2-to-1 sub-protocol uses the last coordinate of the $i$-th group (the input is encoded in the previous coordinates). That is:
$$\scCRS^i \gets \scGen(1^n, \pp, ((i-1) \cdot \mvars',\mvars'-1)) \quad,\quad \ttoCRS^i \gets \ttoGen(1^n, \pp, i \cdot \mvars' - 1)\enspace,$$

\item $\bbGen$ outputs:
$$\CRS = \(\pp,\set{\(\scCRS^i,\ttoCRS^i\)}_{i \in [\cirD]}\)\enspace.$$
\end{enumerate}

\subsubsection{The prover $\bbP$}
\paragraph{Input:}
\begin{enumerate}
    \item The challenge:
    $$\CRS = \(\pp,\set{\(\scCRS^i,\ttoCRS^i\)}_{i \in [\cirD]}\)\enspace.$$
    \item The function $\func$ described by the ring-independent arithmetic circuits:
    $$\set{\EFadd_i,\EFsub_i,\EFmult_i}_{i \in \cirD}\enspace$$
    \item The input $\xinp \in \zo^\inpS$ to $\func$.
\end{enumerate}

\noindent For every $i \in [0,\cirD]$ let:
$$\Fcir_i: \zo^\mvars \rightarrow \zo\enspace,$$
be a function such that $\Fcir_i(\gate) = 1$ if $\gate$ is a gate in layer $i$, and the value of $\gate$ in $\func(\xinp)$ is $1$ where we evaluate $\func$ over an arbitrary ring. (Note that since $\func$ is strongly ring-independent, the choice of ring has no effect, and $\Fcir_i$ is a well defined a boolean function).
Let $\EFcir_i$ be a multi-linear, ring-independent arithmetic circuit computing $\Fcir_i$ (see \secref{sec.MLE}).

Let $\vzinp_0 \in\zo^\mvars$ be the output gate of $\func$, and let $\vval_0 = \EFcir_0(\vzinp_0)$.
To prove the statement it is sufficient to prove that $1 = \vval_0$. To this end, for every $i \in [\cirD]$, $\bbP$ obtains encoded values $\vzinp_i,\vval_i$ and provides a proof $\Proof_i$ for the fact that:
$$\vval_i = \EFcir_i(\vzinp_i) \quad \Rightarrow \quad \vval_{i-1} = \EFcir_{i-1}(\vzinp_{i-1})\enspace.$$
The last statement $\vval_\cirD = \EFcir_\cirD(\vzinp_\cirD)$  can be verified directly by $\bbV$.

For every $i \in [0,\cirD]$ let
$$\vzinp_i = (\zinp_{i,1},\dots,\zinp_{i,\mvars}) \in \zo^\mvars \enspace,$$
For every $j \in [\mvars]$, let $\vlevel_{i,j}$ be the level under which the value $\zinp_{i,j}$ is encoded and let $\vlevel_i$ be the level under which the value $\vval_i$ is encoded.
We require that:
\begin{align}\label{eq.vilsvij}
\vlevel_i \geq \sum_{j \in[\mvars]}{\vlevel_{i,j}}\enspace.
\end{align}
$\bbP$ sets $\vlevel_{0}$ and $\vlevel_{0,j}$ for every $j \in [\mvars]$ to the all-zero level. (Note that \eqnref{eq.vilsvij} is satisfied.)
Using the operation $\Enc$, $\bbP$ obtains the encodings:
$$\set{\enc{\zinp_{0,j}}{\vlevel_{0,j}}}_{j \in [\mvars]} \quad,\quad \enc{\vval_0}{\vlevel_0}\enspace.$$
For every $i \in [\cirD]$ starting from $i=1$, $\bbP$ obtains the encoded values $\vzinp_i,\vval_i$ and the proof $\Proof_i$ as follows.

\begin{enumerate}
\item
Let $\gfunc_i$ be an arithmetic circuit computing the following expression:
\begin{align*}
\gfunc_i(\vwinp_1) = \sum_{\vwinp_2,\vwinp_3 \in \zo^\mvars}\(
\begin{array}{cl}
&\EFadd_i(\vwinp_1,\vwinp_2,\vwinp_3) \cdot \(\EFcir_i(\vwinp_2) + \EFcir_i(\vwinp_3)\)\\
+&\EFsub_i(\vwinp_1,\vwinp_2,\vwinp_3) \cdot \(\EFcir_i(\vwinp_2) - \EFcir_i(\vwinp_3)\)\\
+&\EFmult_i(\vwinp_1,\vwinp_2,\vwinp_3) \cdot \(\EFcir_i(\vwinp_2) \cdot \EFcir_i(\vwinp_3)\)\\
\end{array}
\)\enspace.
\end{align*}

Since the circuits $\EFadd_i, \EFsub_i, \EFmult_i, \EFcir_i$ are all ring-independent, we have that following holds over any field:
\begin{align*}
\gfunc_i(\vwinp_1) = \sum_{\vwinp_2,\vwinp_3 \in \zo^\mvars}\(
\begin{array}{cl}
&\Fadd_i(\vwinp_1,\vwinp_2,\vwinp_3) \cdot \(\Fcir_i(\vwinp_2) + \Fcir_i(\vwinp_3)\)\\
+&\Fsub_i(\vwinp_1,\vwinp_2,\vwinp_3) \cdot \(\Fcir_i(\vwinp_2) - \Fcir_i(\vwinp_3)\)\\
+&\Fmult_i(\vwinp_1,\vwinp_2,\vwinp_3) \cdot \(\Fcir_i(\vwinp_2) \cdot \Fcir_i(\vwinp_3)\)\\
\end{array}
\)\enspace.
\end{align*}
Therefore, by the definition of the functions:
$$\Fadd_i, \Fsub_i, \Fmult_i, \Fcir_i, \Fcir_{i-1}\enspace,$$
we have that the following holds over any ring:
$$\gfunc_i(\vwinp_1) = \Fcir_{i-1}(\vwinp_1)\enspace.$$
(Recall that since $\func$ is strongly ring-independent, $\Fcir_{i-1}(\vwinp_1)$ is independent of the ring over which $\func$ is evaluated.)
Following the discussion in \secref{sec.MLE} and \eqnref{eq.mle}, we have that the following holds over any ring:
\begin{align}\label{eq.usefi}
\EFcir_{i-1}(\vzinp) \equiv \sum_{\vwinp_1 \in \zo^n}{\Iden_n(\vzinp,\vwinp_1) \cdot \gfunc_i(\vwinp_1)} \equiv \sum_{\vwinp_1,\vwinp_2,\vwinp_3 \in \zo^n}{\func_i(\vzinp,\vwinp_1,\vwinp_2,\vwinp_3)}\enspace.
\end{align}
where:
\begin{align}\label{eq.deffi}
\func_i(\vzinp,\vwinp_1,\vwinp_2,\vwinp_3) = \Iden(\vzinp,\vwinp_1)\cdot\(
\begin{array}{cl}
&\EFadd_i(\vwinp_1,\vwinp_2,\vwinp_3) \cdot \(\EFcir_i(\vwinp_2) + \EFcir_i(\vwinp_3)\)\\
+&\EFsub_i(\vwinp_1,\vwinp_2,\vwinp_3) \cdot \(\EFcir_i(\vwinp_2) - \EFcir_i(\vwinp_3)\)\\
+&\EFmult_i(\vwinp_1,\vwinp_2,\vwinp_3) \cdot \(\EFcir_i(\vwinp_2) \cdot \EFcir_i(\vwinp_3)\)\\
\end{array}
\)\enspace.
\end{align}




$\bbP$ executes the sum-check prover:
$$\scP\(\pp, \scCRS^i, \func_i, \scins^i\)\enspace,$$
where:
$$\scins^i = \(\set{\enc{\zinp_{i-1,j}}{\vlevel_{i-1,j}}}_{j \in[\mvars]}, \enc{\vval_{i-1}}{\vlevel_{i-1}}\)\enspace.$$
Note that $\func_i$ is of individual degree 1 in its first $\mvars$ variables, and of individual degree at most $\edegree + 3$ in all of its other variables, therefore it follows from \eqnref{eq.vilsvij} that the input to $\scP$ satisfies the requirements described in \secref{sec.sc}.

$\bbP$ obtains an encoded output:
$$\scinso^i = \(\set{\enc{\winp_{i,j}}{\elevel_{(i-1) \cdot \mvars' + j}}}_{j\in [3\mvars]},\enc{\vvalo_i}{\vlevel_i + (\edegree + 3) \cdot \ulevel_i}\)\enspace,$$
where:
$$\ulevel_i = \sum_{j \in [3\mvars]}{\elevel_{(i-1) \cdot \mvars' + j}}\enspace.$$

$\bbP$ also obtains a sum-check proof $\scProof^i$ for the fact that:
\begin{align*}
\vvalo_i = \func_i(\vzinp_{i-1},\vwinp_{i,1},\vwinp_{i,2},\vwinp_{i,3})\quad \Rightarrow \quad \vval_{i-1} = \sum_{\vwinp_1,\vwinp_2,\vwinp_3 \in \zo^\mvars}{\func_i(\vzinp_{i-1},\vwinp_1,\vwinp_2,\vwinp_3)} \enspace,
\end{align*}
where:
\begin{align*}
\vwinp_{i,1} &= (\winp_{i,1},\dots,\winp_{i,\mvars})\enspace,\\
\vwinp_{i,2} &= (\winp_{i,\mvars + 1},\dots,\winp_{i,2\mvars})\enspace,\\
\vwinp_{i,3} &= (\winp_{i,2\mvars + 1},\dots,\winp_{i,3\mvars})\enspace.
\end{align*}

\item
To prove that:
\begin{align*}
\vvalo_i = \func_i(\vzinp_{i-1},\vwinp_{i,1},\vwinp_{i,2},\vwinp_{i,3})\enspace,
\end{align*}
$\bbP$ uses the arithmetic circuits $\EFadd_i,\EFsub_i,\EFmult_i$ and the operations $\Enc,\Add,\Sub,\Mult$ to obtains the encodings:
$$\enc{\vvala_i}{\edegree \cdot \ulevel_i}, \enc{\vvals_i}{\edegree \cdot \ulevel_i}, \enc{\vvalm_i}{\edegree \cdot \ulevel_i}, \enc{\vval^1_i}{\ulevel_i}, \enc{\vval^2_i}{\ulevel_i}$$
where:
\begin{align*}
\begin{array}{cl}
\vvala_i &= \EFadd_i(\vwinp_{i,1},\vwinp_{i,2},\vwinp_{i,3})\enspace,\\
\vvals_i &= \EFsub_i(\vwinp_{i,1},\vwinp_{i,2},\vwinp_{i,3})\enspace,\\
\vvalm_i &= \EFmult_i(\vwinp_{i,1},\vwinp_{i,2},\vwinp_{i,3})\enspace.
\end{array}
\end{align*}
and:
\begin{align}\label{eq.bbpcs2}
\begin{array}{cl}
\vval^1_i &= \EFcir_i(\vwinp_{i,2})\enspace, \\
\vval^2_i &= \EFcir_i(\vwinp_{i,3})\enspace.
\end{array}
\end{align}
(The levels of the these encodings are derived from the fact that $\EFadd_i,\EFsub_i,\EFmult_i$ are of individual degree $\edegree$ in every variable and $\EFcir_i$ is multi-linear by \eqnref{eq.vilsvij}.)

\item
Using the operation $\Enc$, $\bbP$ obtains the encodings:
$$\set{\enc{\winp_{i,\mvars + j}}{\ulevel_{i,j}},\enc{\winp_{i,2\mvars + j}}{\ulevel_{i,j}}}_{j \in [\mvars]} \enspace,$$
where:
$$\ulevel_{i,j} = \elevel_{(i-1) \cdot \mvars' + j} + \elevel_{(i-1) \cdot \mvars' + \mvars + j} + \elevel_{(i-1) \cdot \mvars' + 2\mvars + j}\enspace.$$

To prove that \eqnref{eq.bbpcs2} holds, $\bbP$ executes the 2-to-1 prover:
$$\ttoP\(\pp, \ttoCRS^i, \EFcir_i, \ttoins^i\)\enspace,$$
where:
$$\ttoins^i = \(\set{\enc{\winp_{i,\mvars + j}}{\ulevel_{i,j}},\enc{\winp_{i,2\mvars + j}}{\ulevel_{i,j}}}_{j \in [\mvars]}, \enc{\vval^1_i}{\ulevel_i}, \enc{\vval^2_i}{\ulevel_i}\)\enspace.$$
Note that $\EFcir_i$ is multi-linear and that:
$$\sum_{j \in [\mvars]}{\ulevel_{i,j}} = \ulevel_i \enspace.$$
Therefore, the input to $\ttoP$ satisfies the requirements described in \secref{sec.sc}.

$\bbP$ obtains an encoded output:
$$\ttoinso^i = \(\set{\enc{\zinp_{i,j}}{\vlevel_{i,j}}}_{j \in [\mvars]}, \enc{\vval_i}{\vlevel_i}\)\enspace,$$
where:
$$\vlevel_{i,j} = \ulevel_{i,j} + \elevel_{i \cdot \mvars'} \quad,\quad \vlevel_i = \ulevel_i + \mvars \cdot \elevel_{i \cdot \mvars'}\enspace.$$
(Note that \eqnref{eq.vilsvij} is satisfied.)

$\bbP$ also obtains a 2-to-1 proof $\ttoProof^i$ for the fact that:
\begin{align*}
\vval_i = \EFcir_i(\vzinp_i) \quad \Rightarrow \quad \eqref{eq.bbpcs2}\enspace,
\end{align*}

\end{enumerate}

\noindent Finally, $\bbP$ outputs the public parameters $\pp$, the encoded output:
$$\inso = \(\set{\enc{\winp_{i,j}}{\elevel_{(i-1) \cdot \mvars' + j}}}_{i \in [\cirD], j \in [\mvars'-1]} ,\set{\enc{\vvala_i}{\edegree \cdot \ulevel_i}, \enc{\vvals_i}{\edegree \cdot \ulevel_i}, \enc{\vvalm_i}{\edegree \cdot \ulevel_i}}_{i \in [\cirD]}\)\enspace,$$
and the proof:
$$\Proof = \set{\Proof_i}_{i \in [\cirD]} = \set{\(\scins^i,\ttoins^i,\scinso^i,\ttoinso^i,\scProof^i,\ttoProof^i\)}_{i \in [\cirD]}\enspace.$$

\subsubsection{The verifier $\bbV$}
\paragraph{Input:}
\begin{enumerate}
    \item The challenge:
    $$\CRS = \(\pp,\set{\(\scCRS^i,\ttoCRS^i\)}_{i \in [\cirD]}\)\enspace.$$
    \item The input $\xinp \in \zo^\inpS$ to $\func$.
    \item The public parameters $\pp$.
    \item The encoded output:
    $$\inso = \(\set{\enc{\winp_{i,j}}{\elevel_{(i-1) \cdot \mvars' + j}}}_{i \in [\cirD], j \in [\mvars'-1]} ,\set{\enc{\vvala_i}{\edegree \cdot \ulevel_i}, \enc{\vvals_i}{\edegree \cdot \ulevel_i}, \enc{\vvalm_i}{\edegree \cdot \ulevel_i}}_{i \in [\cirD]}\)\enspace.$$
    \item The proof:
    $$\Proof = \set{\(\scins^i,\ttoins^i,\scinso^i,\ttoinso^i,\scProof^i,\ttoProof^i\)}_{i \in [\cirD]}\enspace.$$
\end{enumerate}

\noindent Let $\vzinp_0 \in \zo^\mvars$ be the output gate of $\func$ and let $\vval_0 = 1$.
Using the operation $\Enc$, $\bbV$ obtains the encodings:
$$\set{\enc{\zinp_{0,j}}{\vlevel_{0,j}}}_{j \in [\mvars]} \quad,\quad \enc{\vval_0}{\vlevel_0}\enspace.$$

For every $i \in [\cirD]$, let:
\begin{align*}
\scins^i &= \(\set{\enc{\zinp'_{i-1,j}}{\vlevel_{i-1,j}}}_{j \in[\mvars]}, \enc{\vval'_{i-1}}{\vlevel_{i-1}}\)\enspace, \\
\scinso^i &= \(\set{\enc{\winp'_{i,j}}{\elevel_{(i-1) \cdot \mvars' + j}}}_{j\in [3\mvars]},\enc{\vvalo_i}{\vlevel_i + (\edegree + 3) \cdot \ulevel_i}\)\enspace, \\
\ttoins^i &= \(\set{\enc{\winp''_{i,\mvars + j}}{\ulevel_{i,j}},\enc{\winp''_{i,2\mvars + j}}{\ulevel_{i,j}}}_{j \in [\mvars]}, \enc{\vval^1_i}{\ulevel_i}, \enc{\vval^2_i}{\ulevel_i}\)\enspace,\\
\ttoinso^i &= \(\set{\enc{\zinp_{i,j}}{\vlevel_{i,j}}}_{j \in [\mvars]}, \enc{\vval_i}{\vlevel_i}\)\enspace.
\end{align*}

For every $i \in [\cirD]$, $\bbV$ performs the following tests:
\begin{enumerate}
\item \label{tst.bbvt1}
$\bbV$ uses the operations $\Sub, \isZero$ to verify that:
$$\forall j \in [\mvars]: \zinp'_{i-1,j} = \zinp_{i-1,j} \quad , \quad \vval'_{i-1} = \vval_{i-1} \enspace.$$

\item \label{tst.bbvt2}
$\bbV$ verifies that the $i$-th sum-check proof is accepting:
$$1 \gets \scV(\pp, \scCRS^i, \scins^i , \scinso^i, \scProof^1) \enspace.$$

\item \label{tst.bbvt3}
$\bbV$ uses the operations $\Sub, \isZero$ to verify that:
$$\forall j \in [3\mvars]: \winp'_{i,j} = \winp_{i,j}\enspace.$$

\item \label{tst.bbvt4}
$\bbV$ uses the operations $\Add,\Sub,\Mult,\isZero$ to verify that:
$$\vvalo_i = \Iden(\zinp'_{i-1,1},\dots,\zinp'_{i-1,\mvars},\winp_{i,1},\dots,\winp_{i,\mvars})\cdot\(\vvala_i \cdot \(\vval^1_i + \vval^2_i\) + \vvals_i \cdot \(\vval^1_i - \vval^2_i\) + \vvalm_i \cdot \(\vval^1_i \cdot \vval^2_i\)
\)\enspace. $$

\item \label{tst.bbvt5}
$\bbV$ uses the operations $\Sub, \isZero$ to verify that:
$$\forall j \in [\mvars]: \winp''_{i,\mvars +j} = \winp'_{i,\mvars +j} \quad \land \quad \winp''_{i,2\mvars +j} = \winp'_{i,2\mvars +j}\enspace.$$

\item \label{tst.bbvt6}
$\bbV$ verifies that the $i$-th 2-to-1 proof is accepting:
$$1 \gets \ttoV(\pp, \ttoCRS^i, \ttoins^i , \ttoinso^i, \ttoProof^1) \enspace.$$
\end{enumerate}

\noindent Finally, following \eqnref{eq.mle}, $\bbV$ uses the input $\xinp$ and the operation $\Enc,\Add,\Sub,\Mult, \isZero$ to verify that:
\begin{align}\label{eq.bbvt7}
\vval_\cirD = \EFcir_\cirD(\zinp_{\cirD,1},\dots,\zinp_{\cirD,\mvars}) \enspace.
\end{align}
(Note that in \eqnref{eq.mle}, only $|\xinp|$ of the summands are non-zero .

$\bbV$ accepts iff all tests pass.

\subsection{Proof of \clmref{clm.bbas}}
Let $(\cPins, \cPproof)$ be a pair of poly-size circuits. We prove that there exists a negligible function $\mu$ such that for every security parameter $n \in \Nat$:
$$\Pr\[
    \begin{array}{l}
        \CRS \gets \bbGen(1^n,\edegree,\mvars); \\
        \func, \xinp \gets \cPins();\\
        \pp,\insc,\cProof \gets \cPproof(\CRS,\func, \xinp); \\
        1 \gets \bbV(\CRS, \xinp, \pp, \insc, \cProof);\\
        \Echeat
    \end{array}
\] \leq \mu(n)\enspace.$$
where $\func$ is given by the arithmetic circuits:
$$\set{\EFadd_i,\EFsub_i,\EFmult_i}_{i \in \cirD}\enspace,$$
and
$$\insc = \(\set{\enc{\winp_{i,j}}{\elevel_{(i-1) \cdot \mvars' + j}}}_{i \in [\cirD], j \in [\mvars'-1]} ,\set{\enc{\vvala_i}{\edegree \cdot \ulevel_i}, \enc{\vvals_i}{\edegree \cdot \ulevel_i}, \enc{\vvalm_i}{\edegree \cdot \ulevel_i}}_{i \in [\cirD]}\)\enspace,$$
and $\Echeat$ is the event that:
$$ \(\forall i \in [\cirD]:\(\EFadd_i(\vwinp_i) = \vvala_i\) \land \(\EFsub_i(\vwinp_i) = \vvals_i\) \land \(\EFmult_i(\vwinp_i) = \vvalm_i\)\) \quad\not\rightarrow\quad \func(\xinp) = 1 \enspace,$$
where for every $i \in [\cirD]$:
$$\vwinp_i = \(\winp_{i,1},\dots,\winp_{i,\mvars' -1}\)\enspace,$$
and the arithmetic above and in what follows is over the field $\zp$ that is defined by $\pp$.

We start by reintroducing the notations used in the construction. In the above experiment, let:
$$\cProof = \set{\(\scins^i,\ttoins^i,\scinso^i,\ttoinso^i,\scProof^i,\ttoProof^i\)}_{i \in [\cirD]}\enspace,$$
for every $i \in [\cirD]$, let:
\begin{align*}
\scins^i &= \(\set{\enc{\zinp'_{i-1,j}}{\vlevel_{i-1,j}}}_{j \in[\mvars]}, \enc{\vval'_{i-1}}{\vlevel_{i-1}}\)\enspace, \\
\scinso^i &= \(\set{\enc{\winp'_{i,j}}{\elevel_{(i-1) \cdot \mvars' + j}}}_{j\in [3\mvars]},\enc{\vvalo_i}{\vlevel_i + (\edegree + 3) \cdot \ulevel_i}\)\enspace, \\
\ttoins^i &= \(\set{\enc{\winp''_{i,\mvars + j}}{\ulevel_{i,j}},\enc{\winp''_{i,2\mvars + j}}{\ulevel_{i,j}}}_{j \in [\mvars]}, \enc{\vval^1_i}{\ulevel_i}, \enc{\vval^2_i}{\ulevel_i}\)\enspace,\\
\ttoinso^i &= \(\set{\enc{\zinp_{i,j}}{\vlevel_{i,j}}}_{j \in [\mvars]}, \enc{\vval_i}{\vlevel_i}\)\enspace,
\end{align*}
and let:
\begin{align*}
\vzinp_i &= \(\zinp_{i,1},\dots,\zinp_{i,\mvars}\) \enspace,\\
\vzinp'_i &= \(\zinp'_{i,1},\dots,\zinp'_{i,\mvars}\) \enspace,\\
\vwinp'_i &= \(\winp'_{i,1},\dots,\winp'_{i,3\mvars}\) \enspace,\\
\vwinp''_{i,2} &= \(\winp''_{i,\mvars + 1},\dots,\winp''_{i,2\mvars}\) \enspace,\\
\vwinp''_{i,3} &= \(\winp''_{i,2\mvars1},\dots,\winp''_{i,3\mvars}\)\enspace.
\end{align*}

For every $i \in [0,\cirD]$ let $\EFcir_i$ be defined as in the honest prover strategy $\bbP$ with respect to $\func,\xinp$ generated by $\cPins$.
For every $i \in [\cirD]$ let $\func_i$ be defined as in \eqnref{eq.deffi}.

Let $\scEcheat^i$ be the event:
$$\func_i(\vzinp'_{i-1},\vwinp'_i) = \vvalo_i \quad\not\rightarrow\quad \sum_{\vwinp \in \zo^{3\mvars}}{\func_i(\vzinp'_{i-1},\vwinp_i)} = \vval'_{i-1} \enspace,$$
let $\ttoEcheat^i$ be the event:
$$\EFcir_i(\vzinp_i) = \vval_i \quad\not\rightarrow\quad  \(\EFcir_i(\vwinp''_{i,2}) = \vval^1_i \quad \land \quad \EFcir_i(\vwinp''_{i,3}) = \vval^2_i\) \enspace,$$
and let $\Eout^i$ be the event:
$$\(\EFadd_i(\vwinp_i) = \vvala_i\) \land \(\EFsub_i(\vwinp_i) = \vvals_i\) \land \(\EFmult_i(\vwinp_i) = \vvalm_i\)\enspace.$$
Let $\ES$ be the event that in the above experiment, the verifier $\bbV$ accepts the proof $\cProof$.
When $\ES$ occurs, \eqnref{eq.bbvt7} holds:
$$\vval_\cirD = \EFcir_\cirD(\zinp_{\cirD,1},\dots,\zinp_{\cirD,\mvars}) \enspace.$$
We will show that there exist negligible function $\mu_1$ such that for every $i \in [\cirD]$:
\begin{align}\label{eq.bba1}
\Pr\[\ES \land \Eout^i \land \vval_i = \EFcir_i(\vzinp_i) \quad\not\rightarrow\quad \vval_{i-1} = \EFcir_{i-1}(\vzinp_{i-1})\]\leq \mu_1(n)\enspace.
\end{align}
Since $\vzinp_0$ is the output gate of $\func$ and $\vval_0 = 1$, it follows by union bound that:
$$\Pr\[\ES \land \Echeat\] = \Pr\[\ES \land \Eout^1 \land \dots \land \Eout^\cirD \quad\not\rightarrow\quad  \EFcir_i(\vzinp_0) = 1\] \leq \cirD \cdot \mu_1(n)\enspace,$$
as required.

In the rest of the proof we will prove \eqnref{eq.bba1}.
To this end, we assume that:
$$\ES \quad\land\quad \Eout^i \quad\land\quad \vval_i = \EFcir_i(\vzinp_i) \enspace,$$
and we prove that:
$$\Pr\[\vval_{i-1} = \EFcir_{i-1}(\vzinp_{i-1})\] \geq 1- \mu_1(n)\enspace.$$

Since $\bbV$ accepts the 2-to-1 proof $\ttoProof^i$ (\tstref{tst.bbvt6}), it follows from \clmref{clm.ttoas} that for some negligible function $\mu_2$:
$$\Pr\[\ttoEcheat^i\] = \Pr\[\EFcir_i(\vzinp_i) = \vval_i \quad\not\rightarrow\quad \(\EFcir_i(\vwinp''_{i,2}) = \vval^1_i \quad \land \quad \EFcir_i(\vwinp''_{i,3}) = \vval^2_i\)\] \leq \mu_2(n)\enspace.$$
By our assumption $\vval_i = \EFcir_i(\vzinp_i)$ and therefore:
$$\Pr\[\EFcir_i(\vwinp''_{i,2}) = \vval^1_i \quad \land \quad \EFcir_i(\vwinp''_{i,3}) = \vval^2_i\] \geq 1- \mu_2(n)\enspace.$$
Since $\bbV$'s \tstref{tst.bbvt5} passes:
$$\Pr\[\EFcir_i(\vwinp_{i,2}) = \vval^1_i \quad \land \quad \EFcir_i(\vwinp_{i,3}) = \vval^2_i\] \geq 1- \mu_2(n)\enspace,$$
where
$$\vwinp_{i,2} = \(\winp_{i,\mvars + 1},\dots,\winp_{i,2\mvars}\) \quad,\quad \vwinp_{i,3} = \(\winp_{i,2\mvars + 1},\dots,\winp_{i,3\mvars}\) \enspace.$$
Together with the definition of $\func_i$ and the assumption that $\Eout^i$ holds and \tstref{tst.bbvt4} passes we get that:
$$\Pr\[\vvalo_i = \func_i(\vzinp'_{i-1},\vwinp_i)\] \geq 1- \mu_2(n)\enspace,$$
and since $\bbV$'s \tstref{tst.bbvt3} passes:
$$\Pr\[\vvalo_i = \func_i(\vzinp'_{i-1},\vwinp'_i)\] \geq 1- \mu_2(n)\enspace.$$

Since $\bbV$ accepts the sum-check proof $\scProof^i$ (\tstref{tst.bbvt2}), it follows from \clmref{clm.scas} that for some negligible function $\mu_3$:
$$\Pr\[\scEcheat^i\] = \Pr\[\func_i(\vzinp'_{i-1},\vwinp'_i) = \vvalo_i \quad\not\rightarrow\quad \sum_{\vwinp \in \zo^{3\mvars}}{\func_i(\vzinp'_{i-1},\vwinp_i)} = \vval'_{i-1}\] \leq \mu_3(n)\enspace.$$
By union bound, we have that for $\mu_1 = \mu_2 + \mu_3$:
$$\Pr\[\sum_{\vwinp \in \zo^{3\mvars}}{\func_i(\vzinp'_{i-1},\vwinp_i)} = \vval'_{i-1}\] \geq 1- \mu_1(n)\enspace,$$
and since \eqnref{eq.usefi} holds over any ring (see discussion in the definition of the prover $\bbP$), in particular over $\zp$:
$$\Pr\[\EFcir_{i-1}(\vzinp'_{i-1}) = \vval'_{i-1}\] \geq 1- \mu_1(n)\enspace.$$
Finally, since $\bbV$'s \tstref{tst.bbvt1} passes we get the required:
$$\Pr\[\EFcir_{i-1}(\vzinp_{i-1}) = \vval_{i-1}\] \geq 1- \mu_1(n)\enspace.$$

\bibliographystyle{alpha}
{
\bibliography{fs-delegation}
}

\end{document}



